diff --git a/Arm/Memory/MemOmega.lean b/Arm/Memory/MemOmega.lean
index f52dd3c3..7b9426ff 100644
--- a/Arm/Memory/MemOmega.lean
+++ b/Arm/Memory/MemOmega.lean
@@ -96,25 +96,29 @@ def memOmega (g : MVarId) : MemOmegaM Unit := do
         catch e =>
           trace[simp_mem.info]  "{crossEmoji} `omega` failed with error:\n{e.toMessageData}"
 
+syntax memOmegaRule := term
+
 /--
 Allow elaboration of `MemOmegaConfig` arguments to tactics.
 -/
 declare_config_elab elabMemOmegaConfig MemOmega.Config
 
+syntax memOmegaUsing := &"using" "[" withoutPosition(memOmegaRule,*,?) "]"
+
 /--
-Implement the `mem_omega` tactic, which unfolds information about memory
-in terms of
+Implement the `mem_omega` tactic, which unfolds information about memory and then closes the goal state using `omega`.
 -/
-syntax (name := mem_omega) "mem_omega" (Lean.Parser.Tactic.config)? : tactic
+syntax (name := mem_omega) "mem_omega" (Lean.Parser.Tactic.config)? (memOmegaUsing)?  : tactic
 
 /--
 Implement the `mem_omega` tactic frontend.
 -/
-syntax (name := mem_omega_bang) "mem_omega!" (Lean.Parser.Tactic.config)? : tactic
+syntax (name := mem_omega_bang) "mem_omega!" (memOmegaUsing)?  : tactic
 
+open Lean.Parser.Tactic in
 @[tactic mem_omega]
-def evalMemOmega : Tactic := fun
-  | `(tactic| mem_omega $[$cfg]?) => do
+def evalMemOmega : Tactic := fun 
+  | `(tactic| mem_omega $[$cfg:config]? $[$v:memOmegaUsing]?) => do
     let cfg ← elabMemOmegaConfig (mkOptionalNode cfg)
     liftMetaFinishingTactic fun g => do
       memOmega g |>.run (← Context.init cfg)