--- a/src/HOL/IMP/Abs_Int0_fun.thy Wed Oct 19 23:07:48 2011 +0200
+++ b/src/HOL/IMP/Abs_Int0_fun.thy Thu Oct 20 09:48:00 2011 +0200
@@ -11,11 +11,11 @@
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
@@ -300,7 +300,7 @@
end
-type_synonym 'a st = "(name \<Rightarrow> 'a)"
+type_synonym 'a st = "(vname \<Rightarrow> 'a)"
locale Abs_Int_Fun = Val_abs
begin