# HG changeset patch
# User nipkow
# Date 1324374153 -3600
# Node ID 2cae3d86abe5e42bbdd670c4bc7668246718b9e6
# Parent  d7eabc09b6389cf57f8c50d1e3d5089d6db0efcc
tuned

diff -r d7eabc09b638 -r 2cae3d86abe5 src/HOL/IMP/Collecting.thy
--- a/src/HOL/IMP/Collecting.thy	Mon Dec 19 17:10:53 2011 +0100
+++ b/src/HOL/IMP/Collecting.thy	Tue Dec 20 10:42:33 2011 +0100
@@ -63,30 +63,30 @@
 
 end
 
-fun sub1 :: "'a acom \<Rightarrow> 'a acom" where
-"sub1(c1;c2) = c1" |
-"sub1(IF b THEN c1 ELSE c2 {S}) = c1" |
-"sub1({I} WHILE b DO c {P}) = c"
+fun sub\<^isub>1 :: "'a acom \<Rightarrow> 'a acom" where
+"sub\<^isub>1(c1;c2) = c1" |
+"sub\<^isub>1(IF b THEN c1 ELSE c2 {S}) = c1" |
+"sub\<^isub>1({I} WHILE b DO c {P}) = c"
 
-fun sub2 :: "'a acom \<Rightarrow> 'a acom" where
-"sub2(c1;c2) = c2" |
-"sub2(IF b THEN c1 ELSE c2 {S}) = c2"
+fun sub\<^isub>2 :: "'a acom \<Rightarrow> 'a acom" where
+"sub\<^isub>2(c1;c2) = c2" |
+"sub\<^isub>2(IF b THEN c1 ELSE c2 {S}) = c2"
 
 fun invar :: "'a acom \<Rightarrow> 'a" where
 "invar({I} WHILE b DO c {P}) = I"
 
-fun lift :: "('a set set \<Rightarrow> 'a set) \<Rightarrow> com \<Rightarrow> 'a set acom set \<Rightarrow> 'a set acom"
+fun lift :: "('a set \<Rightarrow> 'a) \<Rightarrow> com \<Rightarrow> 'a acom set \<Rightarrow> 'a acom"
 where
 "lift F com.SKIP M = (SKIP {F (post ` M)})" |
 "lift F (x ::= a) M = (x ::= a {F (post ` M)})" |
 "lift F (c1;c2) M =
-  lift F c1 (sub1 ` M); lift F c2 (sub2 ` M)" |
+  lift F c1 (sub\<^isub>1 ` M); lift F c2 (sub\<^isub>2 ` M)" |
 "lift F (IF b THEN c1 ELSE c2) M =
-  IF b THEN lift F c1 (sub1 ` M) ELSE lift F c2 (sub2 ` M)
+  IF b THEN lift F c1 (sub\<^isub>1 ` M) ELSE lift F c2 (sub\<^isub>2 ` M)
   {F (post ` M)}" |
 "lift F (WHILE b DO c) M =
  {F (invar ` M)}
- WHILE b DO lift F c (sub1 ` M)
+ WHILE b DO lift F c (sub\<^isub>1 ` M)
  {F (post ` M)}"
 
 interpretation Complete_Lattice_ix "%c. {c'. strip c' = c}" "lift Inter"