src/HOL/IMP/Abs_Int0_fun.thy

 
 subsection "Annotated Commands"
 
 datatype 'a acom =
   SKIP   'a                           ("SKIP {_}") |
-  Assign name aexp 'a                 ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
-  Semi   "'a acom" "'a acom"          ("_;//_"  [60, 61] 60) |
-  If     bexp "'a acom" "'a acom" 'a
+  Assign vname aexp 'a                ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
+  Semi   "('a acom)" "('a acom)"          ("_;//_"  [60, 61] 60) |
+  If     bexp "('a acom)" "('a acom)" 'a
     ("(IF _/ THEN _/ ELSE _//{_})"  [0, 0, 61, 0] 61) |
-  While  'a bexp "'a acom" 'a
+  While  'a bexp "('a acom)" 'a
     ("({_}//WHILE _/ DO (_)//{_})"  [0, 0, 61, 0] 61)
 
 fun post :: "'a acom \<Rightarrow>'a" where
 "post (SKIP {P}) = P" |
 "post (x ::= e {P}) = P" |

 lemma in_rep_Top[simp]: "x <: \<top>"
 by(simp add: rep_Top)
 
 end
 
-type_synonym 'a st = "(name \<Rightarrow> 'a)"
+type_synonym 'a st = "(vname \<Rightarrow> 'a)"
 
 locale Abs_Int_Fun = Val_abs
 begin
 
 fun aval' :: "aexp \<Rightarrow> 'a st \<Rightarrow> 'a" where