src/HOL/Hoare/Separation.thy

--- a/src/HOL/Hoare/Separation.thy	Wed Feb 10 19:37:34 2010 +0100
+++ b/src/HOL/Hoare/Separation.thy	Wed Feb 10 23:53:46 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Hoare/Separation.thy
-    ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   2003 TUM
 
@@ -50,10 +49,10 @@
 bound Hs - otherwise they may bind the implicit H. *}
 
 syntax
- "@emp" :: "bool" ("emp")
- "@singl" :: "nat \<Rightarrow> nat \<Rightarrow> bool" ("[_ \<mapsto> _]")
- "@star" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "**" 60)
- "@wand" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "-*" 60)
+ "_emp" :: "bool" ("emp")
+ "_singl" :: "nat \<Rightarrow> nat \<Rightarrow> bool" ("[_ \<mapsto> _]")
+ "_star" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "**" 60)
+ "_wand" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "-*" 60)
 
 (* FIXME does not handle "_idtdummy" *)
 ML{*
@@ -79,8 +78,8 @@
 *}
 
 parse_translation
- {* [("@emp", emp_tr), ("@singl", singl_tr),
-     ("@star", star_tr), ("@wand", wand_tr)] *}
+ {* [("_emp", emp_tr), ("_singl", singl_tr),
+     ("_star", star_tr), ("_wand", wand_tr)] *}
 
 text{* Now it looks much better: *}
 
@@ -121,13 +120,13 @@
 *)
   | strip (Abs(_,_,(t as Const("_var",_) $ Var _) $ Bound 0)) = t
   | strip (Abs(_,_,P)) = P
-  | strip (Const("is_empty",_)) = Syntax.const "@emp"
+  | strip (Const("is_empty",_)) = Syntax.const "_emp"
   | strip t = t;
 in
-fun is_empty_tr' [_] = Syntax.const "@emp"
-fun singl_tr' [_,p,q] = Syntax.const "@singl" $ p $ q
-fun star_tr' [P,Q,_] = Syntax.const "@star" $ strip P $ strip Q
-fun wand_tr' [P,Q,_] = Syntax.const "@wand" $ strip P $ strip Q
+fun is_empty_tr' [_] = Syntax.const "_emp"
+fun singl_tr' [_,p,q] = Syntax.const "_singl" $ p $ q
+fun star_tr' [P,Q,_] = Syntax.const "_star" $ strip P $ strip Q
+fun wand_tr' [P,Q,_] = Syntax.const "_wand" $ strip P $ strip Q
 end
 *}