# HG changeset patch
# User wenzelm
# Date 1265842426 -3600
# Node ID 6ce9177d6b38a84f6a28d8038aa7996a7120f0f9
# Parent  53754ec7360b7b70dc7c81a46809d026f7b1c783
modernized translations;

diff -r 53754ec7360b -r 6ce9177d6b38 src/HOL/Hoare/HeapSyntax.thy
--- 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]
diff -r 53754ec7360b -r 6ce9177d6b38 src/HOL/Hoare/HeapSyntaxAbort.thy
--- 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]
diff -r 53754ec7360b -r 6ce9177d6b38 src/HOL/Hoare/HoareAbort.thy
--- 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" *)
 
diff -r 53754ec7360b -r 6ce9177d6b38 src/HOL/Hoare/Pointers0.thy
--- 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"
 
 
diff -r 53754ec7360b -r 6ce9177d6b38 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
 *}
 
diff -r 53754ec7360b -r 6ce9177d6b38 src/HOL/SET_Protocol/Event_SET.thy
--- 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*}