Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authornipkow
Thu, 15 Dec 2011 09:13:32 +0100
changeset 45886 728cc8553471
parent 45884 58a10da12812 (current diff)
parent 45885 19ee710d9c14 (diff)
child 45887 bfb5234a70ba
merged
src/HOL/IsaMakefile file | annotate | diff | comparison | revisions 
--- a/src/HOL/IMP/Collecting.thy	Thu Dec 15 08:51:14 2011 +0100
+++ b/src/HOL/IMP/Collecting.thy	Thu Dec 15 09:13:32 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')"
--- a/src/HOL/IsaMakefile	Thu Dec 15 08:51:14 2011 +0100
+++ b/src/HOL/IsaMakefile	Thu Dec 15 09:13:32 2011 +0100
@@ -527,8 +527,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 \
isabelle