Removed ghost variable syntax, as it's now in Abstract_Prog_Syntax

isabelle-utp · Jan 6, 2025 · c3cdcde · c3cdcde
1 parent 1abd0f4
commit c3cdcde
Showing 1 changed file with 0 additions and 6 deletions.
diff --git a/UTP/ITree_Hoare.thy b/UTP/ITree_Hoare.thy
@@ -4,12 +4,6 @@ theory ITree_Hoare
   imports ITree_WP
 begin
 
-syntax
-  "_ghost_old" :: "id" \<comment> \<open> A distinguished name for the ghost state ("old") \<close>
-
-parse_translation \<open> 
-  [(@{syntax_const "_ghost_old"}, fn ctx => fn term => Syntax.free "old")]\<close>
-
 text \<open> We introduce theorem attributed for safe Hoare rules and already proven triples \<close>
 
 named_theorems hoare_safe and hoare_lemmas