--- a/src/HOL/Hoare/HeapSyntax.thy Wed Feb 10 19:37:34 2010 +0100
+++ b/src/HOL/Hoare/HeapSyntax.thy Wed Feb 10 23:53:46 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Hoare/HeapSyntax.thy
- ID: $Id$
Author: Tobias Nipkow
Copyright 2002 TUM
*)
@@ -9,16 +8,16 @@
subsection "Field access and update"
syntax
- "@refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
+ "_refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
("_/'((_ \<rightarrow> _)')" [1000,0] 900)
- "@fassign" :: "'a ref => id => 'v => 's com"
+ "_fassign" :: "'a ref => id => 'v => 's com"
("(2_^._ :=/ _)" [70,1000,65] 61)
- "@faccess" :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
+ "_faccess" :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
("_^._" [65,1000] 65)
translations
- "f(r \<rightarrow> v)" == "f(addr r := v)"
+ "f(r \<rightarrow> v)" == "f(CONST addr r := v)"
"p^.f := e" => "f := f(p \<rightarrow> e)"
- "p^.f" => "f(addr p)"
+ "p^.f" => "f(CONST addr p)"
declare fun_upd_apply[simp del] fun_upd_same[simp] fun_upd_other[simp]
--- a/src/HOL/Hoare/HeapSyntaxAbort.thy Wed Feb 10 19:37:34 2010 +0100
+++ b/src/HOL/Hoare/HeapSyntaxAbort.thy Wed Feb 10 23:53:46 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Hoare/HeapSyntax.thy
- ID: $Id$
Author: Tobias Nipkow
Copyright 2002 TUM
*)
@@ -17,16 +16,16 @@
reason about storage allocation/deallocation. *}
syntax
- "refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
+ "_refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
("_/'((_ \<rightarrow> _)')" [1000,0] 900)
- "@fassign" :: "'a ref => id => 'v => 's com"
+ "_fassign" :: "'a ref => id => 'v => 's com"
("(2_^._ :=/ _)" [70,1000,65] 61)
- "@faccess" :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
+ "_faccess" :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
("_^._" [65,1000] 65)
translations
- "refupdate f r v" == "f(addr r := v)"
- "p^.f := e" => "(p \<noteq> Null) \<rightarrow> (f := refupdate f p e)"
- "p^.f" => "f(addr p)"
+ "_refupdate f r v" == "f(CONST addr r := v)"
+ "p^.f := e" => "(p \<noteq> CONST Null) \<rightarrow> (f := _refupdate f p e)"
+ "p^.f" => "f(CONST addr p)"
declare fun_upd_apply[simp del] fun_upd_same[simp] fun_upd_other[simp]
--- a/src/HOL/Hoare/HoareAbort.thy Wed Feb 10 19:37:34 2010 +0100
+++ b/src/HOL/Hoare/HoareAbort.thy Wed Feb 10 23:53:46 2010 +0100
@@ -257,7 +257,7 @@
guarded_com :: "bool \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(2_ \<rightarrow>/ _)" 71)
array_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com" ("(2_[_] :=/ _)" [70, 65] 61)
translations
- "P \<rightarrow> c" == "IF P THEN c ELSE Abort FI"
+ "P \<rightarrow> c" == "IF P THEN c ELSE CONST Abort FI"
"a[i] := v" => "(i < CONST length a) \<rightarrow> (a := CONST list_update a i v)"
(* reverse translation not possible because of duplicate "a" *)
--- a/src/HOL/Hoare/Pointers0.thy Wed Feb 10 19:37:34 2010 +0100
+++ b/src/HOL/Hoare/Pointers0.thy Wed Feb 10 23:53:46 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Hoare/Pointers.thy
- ID: $Id$
Author: Tobias Nipkow
Copyright 2002 TUM
@@ -20,12 +19,12 @@
subsection "Field access and update"
syntax
- "@fassign" :: "'a::ref => id => 'v => 's com"
+ "_fassign" :: "'a::ref => id => 'v => 's com"
("(2_^._ :=/ _)" [70,1000,65] 61)
- "@faccess" :: "'a::ref => ('a::ref \<Rightarrow> 'v) => 'v"
+ "_faccess" :: "'a::ref => ('a::ref \<Rightarrow> 'v) => 'v"
("_^._" [65,1000] 65)
translations
- "p^.f := e" => "f := fun_upd f p e"
+ "p^.f := e" => "f := CONST fun_upd f p e"
"p^.f" => "f p"
--- 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
*}
--- a/src/HOL/SET_Protocol/Event_SET.thy Wed Feb 10 19:37:34 2010 +0100
+++ b/src/HOL/SET_Protocol/Event_SET.thy Wed Feb 10 23:53:46 2010 +0100
@@ -11,8 +11,7 @@
begin
text{*The Root Certification Authority*}
-syntax RCA :: agent
-translations "RCA" == "CA 0"
+abbreviation "RCA == CA 0"
text{*Message events*}