# HG changeset patch
# User nipkow
# Date 1323936803 -3600
# Node ID 19ee710d9c14116d3ecceaa1fde540ab7a539fbb
# Parent  dadd139192d172426b0a04d57b99cd1a239d8a07
tuned

diff -r dadd139192d1 -r 19ee710d9c14 src/HOL/IMP/Collecting.thy
--- a/src/HOL/IMP/Collecting.thy	Tue Dec 13 21:15:38 2011 +0100
+++ b/src/HOL/IMP/Collecting.thy	Thu Dec 15 09:13:23 2011 +0100
@@ -15,13 +15,13 @@
 begin
 
 fun less_eq_acom :: "('a::order)acom \<Rightarrow> 'a acom \<Rightarrow> bool" where
-"less_eq_acom (SKIP {S}) (SKIP {S'}) = (S \<le> S')" |
-"less_eq_acom (x ::= e {S}) (x' ::= e' {S'}) = (x=x' \<and> e=e' \<and> S \<le> S')" |
-"less_eq_acom (c1;c2) (c1';c2') = (less_eq_acom c1 c1' \<and> less_eq_acom c2 c2')" |
-"less_eq_acom (IF b THEN c1 ELSE c2 {S}) (IF b' THEN c1' ELSE c2' {S'}) =
-  (b=b' \<and> less_eq_acom c1 c1' \<and> less_eq_acom c2 c2' \<and> S \<le> S')" |
-"less_eq_acom ({Inv} WHILE b DO c {P}) ({Inv'} WHILE b' DO c' {P'}) =
-  (b=b' \<and> less_eq_acom c c' \<and> Inv \<le> Inv' \<and> P \<le> P')" |
+"(SKIP {S}) \<le> (SKIP {S'}) = (S \<le> S')" |
+"(x ::= e {S}) \<le> (x' ::= e' {S'}) = (x=x' \<and> e=e' \<and> S \<le> S')" |
+"(c1;c2) \<le> (c1';c2') = (c1 \<le> c1' \<and> c2 \<le> c2')" |
+"(IF b THEN c1 ELSE c2 {S}) \<le> (IF b' THEN c1' ELSE c2' {S'}) =
+  (b=b' \<and> c1 \<le> c1' \<and> c2 \<le> c2' \<and> S \<le> S')" |
+"({Inv} WHILE b DO c {P}) \<le> ({Inv'} WHILE b' DO c' {P'}) =
+  (b=b' \<and> c \<le> c' \<and> Inv \<le> Inv' \<and> P \<le> P')" |
 "less_eq_acom _ _ = False"
 
 lemma SKIP_le: "SKIP {S} \<le> c \<longleftrightarrow> (\<exists>S'. c = SKIP {S'} \<and> S \<le> S')"
diff -r dadd139192d1 -r 19ee710d9c14 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Dec 13 21:15:38 2011 +0100
+++ b/src/HOL/IsaMakefile	Thu Dec 15 09:13:23 2011 +0100
@@ -520,8 +520,8 @@
   IMP/Abs_Int_Den/Abs_State_den.thy  IMP/Abs_Int_Den/Abs_Int_den0.thy \
   IMP/Abs_Int_Den/Abs_Int_den0_const.thy IMP/Abs_Int_Den/Abs_Int_den1.thy \
   IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy IMP/Abs_Int_Den/Abs_Int_den2.thy \
-  IMP/ASM.thy IMP/AExp.thy IMP/BExp.thy	\
-  IMP/Big_Step.thy IMP/C_like.thy IMP/Com.thy IMP/Compiler.thy \
+  IMP/ASM.thy IMP/AExp.thy IMP/BExp.thy	IMP/Big_Step.thy IMP/C_like.thy \
+  IMP/Collecting.thy IMP/Collecting1.thy IMP/Com.thy IMP/Compiler.thy \
   IMP/Comp_Rev.thy IMP/Def_Ass.thy IMP/Def_Ass_Big.thy IMP/Def_Ass_Exp.thy \
   IMP/Def_Ass_Small.thy IMP/Def_Ass_Sound_Big.thy \
   IMP/Def_Ass_Sound_Small.thy IMP/Denotation.thy IMP/Hoare.thy \