diff --git a/Tactics/StepThms.lean b/Tactics/StepThms.lean
index af788dd2..53dd2e56 100644
--- a/Tactics/StepThms.lean
+++ b/Tactics/StepThms.lean
@@ -8,7 +8,7 @@ import Arm.Map
 import Arm.Decode
 import Tactics.Common
 import Tactics.Simp
-import Tactics.Reflect.ProgramInfo
+import Tactics.Sym.ProgramInfo
 
 open Lean Lean.Expr Lean.Meta Lean.Elab Lean.Elab.Command
 open SymContext (h_pc_type h_program_type h_err_type)
diff --git a/Tactics/Sym.lean b/Tactics/Sym.lean
index 9f08cd6d..5a62f834 100644
--- a/Tactics/Sym.lean
+++ b/Tactics/Sym.lean
@@ -6,7 +6,7 @@ Author(s): Shilpi Goel, Alex Keizer
 import Arm.Exec
 import Arm.Memory.MemoryProofs
 import Tactics.FetchAndDecode
-import Tactics.SymContext
+import Tactics.Sym.Context
 
 import Lean
 
diff --git a/Tactics/Reflect/AxEffects.lean b/Tactics/Sym/AxEffects.lean
similarity index 100%
rename from Tactics/Reflect/AxEffects.lean
rename to Tactics/Sym/AxEffects.lean
diff --git a/Tactics/SymContext.lean b/Tactics/Sym/Context.lean
similarity index 99%
rename from Tactics/SymContext.lean
rename to Tactics/Sym/Context.lean
index dae9d271..b63844f8 100644
--- a/Tactics/SymContext.lean
+++ b/Tactics/Sym/Context.lean
@@ -9,8 +9,8 @@ import Lean.Meta
 import Arm.Exec
 import Tactics.Common
 import Tactics.Attr
-import Tactics.Reflect.ProgramInfo
-import Tactics.Reflect.AxEffects
+import Tactics.Sym.ProgramInfo
+import Tactics.Sym.AxEffects
 import Tactics.Simp
 
 /-!
diff --git a/Tactics/Reflect/FetchAndDecode.lean b/Tactics/Sym/FetchAndDecode.lean
similarity index 98%
rename from Tactics/Reflect/FetchAndDecode.lean
rename to Tactics/Sym/FetchAndDecode.lean
index c9583f20..d584648b 100644
--- a/Tactics/Reflect/FetchAndDecode.lean
+++ b/Tactics/Sym/FetchAndDecode.lean
@@ -5,7 +5,7 @@ Author(s): Alex Keizer
 -/
 import Arm.State
 import Tactics.Common
-import Tactics.Reflect.ProgramInfo
+import Tactics.Sym.ProgramInfo
 
 open Lean Meta
 open Elab.Tactic Elab.Term
diff --git a/Tactics/Reflect/ProgramInfo.lean b/Tactics/Sym/ProgramInfo.lean
similarity index 100%
rename from Tactics/Reflect/ProgramInfo.lean
rename to Tactics/Sym/ProgramInfo.lean
diff --git a/Tests/Tactics/ReduceFetchInst.lean b/Tests/Tactics/ReduceFetchInst.lean
index 630bcbbc..7ff5ae13 100644
--- a/Tests/Tactics/ReduceFetchInst.lean
+++ b/Tests/Tactics/ReduceFetchInst.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Alex Keizer
 -/
-import Tactics.Reflect.FetchAndDecode
+import Tactics.Sym.FetchAndDecode
 import Tests.«AES-GCM».GCMGmultV8Program
 import Tests.SHA2.SHA512Program