diff -r 54a0c675c423 -r 16f424af58a2 src/HOL/UNITY/ProgressSets.thy
--- a/src/HOL/UNITY/ProgressSets.thy	Mon Mar 31 12:29:26 2003 +0200
+++ b/src/HOL/UNITY/ProgressSets.thy	Mon Mar 31 12:29:54 2003 +0200
@@ -141,6 +141,8 @@
 
 
 subsection {*Progress Sets and the Main Lemma*}
+text{*A progress set satisfies certain closure conditions and is a 
+simple way of including the set @{term "wens_set F B"}.*}
 
 constdefs 
   closed :: "['a program, 'a set, 'a set,  'a set set] => bool"
@@ -249,7 +251,9 @@
     by (rule cl_subset_in_lattice [OF cl_subset latt]) 
 qed
 
-text{*The Lemma proved on page 96*}
+text{*Proved on page 96 of Meier's thesis.  The special case when
+   @{term "T=UNIV"} states that every progress set for the program @{term F}
+   and set @{term B} includes the set @{term "wens_set F B"}.*}
 lemma progress_set_lemma:
      "[|C \<in> progress_set F T B; r \<in> wens_set F B; F \<in> stable T|] ==> T\<inter>r \<in> C"
 apply (simp add: progress_set_def, clarify) 
@@ -465,6 +469,7 @@
 
 subsection{*Composition Theorems Based on Monotonicity and Commutativity*}
 
+subsubsection{*Commutativity of @{term "cl L"} and assignment.*}
 constdefs 
   commutes :: "['a program, 'a set, 'a set,  'a set set] => bool"
    "commutes F T B L ==
@@ -472,6 +477,7 @@
            cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T\<inter>M)))"
 
 
+text{*From Meier's thesis, section 4.5.6*}
 lemma commutativity1_lemma:
   assumes commutes: "commutes F T B L" 
       and lattice:  "lattice L"
@@ -490,6 +496,7 @@
 apply (blast intro: rev_subsetD [OF _ wp_mono]) 
 done
 
+text{*Version packaged with @{thm progress_set_Union}*}
 lemma commutativity1:
   assumes leadsTo: "F \<in> A leadsTo B"
       and lattice:  "lattice L"
@@ -528,6 +535,7 @@
 text{*Thesis, page 109*}
 
 (*FIXME: this proof is an ungodly mess*)
+text{*From Meier's thesis, section 4.5.6*}
 lemma commutativity2_lemma:
   assumes dcommutes: 
         "\<forall>act \<in> Acts F. 
@@ -570,6 +578,7 @@
 done
 
 
+text{*Version packaged with @{thm progress_set_Union}*}
 lemma commutativity2:
   assumes leadsTo: "F \<in> A leadsTo B"
       and dcommutes: 
@@ -590,4 +599,7 @@
 done
 
 
+subsection {*Monotonicity*}
+(*to be continued?*)
+
 end