# HG changeset patch
# User huffman
# Date 1323019857 -3600
# Node ID 92c6ddca552ec85e8c3933399dcc682a43aceb3c
# Parent  cf79cc09cab453d8cd6875f66e58eb6a11227f94# Parent  8b05cda62000639c384b36e58a3c006a8ead91d0
merged

diff -r cf79cc09cab4 -r 92c6ddca552e src/HOL/IMP/ACom.thy
--- a/src/HOL/IMP/ACom.thy	Sun Dec 04 13:10:19 2011 +0100
+++ b/src/HOL/IMP/ACom.thy	Sun Dec 04 18:30:57 2011 +0100
@@ -26,11 +26,11 @@
 "post ({Inv} WHILE b DO c {P}) = P"
 
 fun strip :: "'a acom \<Rightarrow> com" where
-"strip (SKIP {a}) = com.SKIP" |
-"strip (x ::= e {a}) = (x ::= e)" |
+"strip (SKIP {P}) = com.SKIP" |
+"strip (x ::= e {P}) = (x ::= e)" |
 "strip (c1;c2) = (strip c1; strip c2)" |
-"strip (IF b THEN c1 ELSE c2 {a}) = (IF b THEN strip c1 ELSE strip c2)" |
-"strip ({a1} WHILE b DO c {a2}) = (WHILE b DO strip c)"
+"strip (IF b THEN c1 ELSE c2 {P}) = (IF b THEN strip c1 ELSE strip c2)" |
+"strip ({Inv} WHILE b DO c {P}) = (WHILE b DO strip c)"
 
 fun anno :: "'a \<Rightarrow> com \<Rightarrow> 'a acom" where
 "anno a com.SKIP = SKIP {a}" |
@@ -42,13 +42,13 @@
   ({a} WHILE b DO anno a c {a})"
 
 fun map_acom :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a acom \<Rightarrow> 'b acom" where
-"map_acom f (SKIP {a}) = SKIP {f a}" |
-"map_acom f (x ::= e {a}) = (x ::= e {f a})" |
+"map_acom f (SKIP {P}) = SKIP {f P}" |
+"map_acom f (x ::= e {P}) = (x ::= e {f P})" |
 "map_acom f (c1;c2) = (map_acom f c1; map_acom f c2)" |
-"map_acom f (IF b THEN c1 ELSE c2 {a}) =
-  (IF b THEN map_acom f c1 ELSE map_acom f c2 {f a})" |
-"map_acom f ({a1} WHILE b DO c {a2}) =
-  ({f a1} WHILE b DO map_acom f c {f a2})"
+"map_acom f (IF b THEN c1 ELSE c2 {P}) =
+  (IF b THEN map_acom f c1 ELSE map_acom f c2 {f P})" |
+"map_acom f ({Inv} WHILE b DO c {P}) =
+  ({f Inv} WHILE b DO map_acom f c {f P})"
 
 
 lemma post_map_acom[simp]: "post(map_acom f c) = f(post c)"
diff -r cf79cc09cab4 -r 92c6ddca552e src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sun Dec 04 13:10:19 2011 +0100
+++ b/src/HOL/IsaMakefile	Sun Dec 04 18:30:57 2011 +0100
@@ -514,7 +514,7 @@
 HOL-IMP: HOL $(OUT)/HOL-IMP
 
 $(OUT)/HOL-IMP: $(OUT)/HOL \
-  IMP/Abs_Int0_fun.thy IMP/Abs_State.thy IMP/Abs_Int0.thy \
+  IMP/ACom.thy IMP/Abs_Int0_fun.thy IMP/Abs_State.thy IMP/Abs_Int0.thy \
   IMP/Abs_Int0_const.thy IMP/Abs_Int1.thy IMP/Abs_Int1_ivl.thy \
   IMP/Abs_Int2.thy IMP/Abs_Int_Den/Abs_Int_den0_fun.thy \
   IMP/Abs_Int_Den/Abs_State_den.thy  IMP/Abs_Int_Den/Abs_Int_den0.thy \