diff -r baefae13ad37 -r 4c1a53627500 src/HOL/UNITY/SubstAx.thy
--- a/src/HOL/UNITY/SubstAx.thy	Thu Jan 30 18:08:09 2003 +0100
+++ b/src/HOL/UNITY/SubstAx.thy	Fri Jan 31 20:12:44 2003 +0100
@@ -6,6 +6,8 @@
 Weak LeadsTo relation (restricted to the set of reachable states)
 *)
 
+header{*Weak Progress*}
+
 theory SubstAx = WFair + Constrains:
 
 constdefs
@@ -27,7 +29,7 @@
 done
 
 
-(*** Specialized laws for handling invariants ***)
+subsection{*Specialized laws for handling invariants*}
 
 (** Conjoining an Always property **)
 
@@ -46,7 +48,7 @@
 lemmas Always_LeadsToD = Always_LeadsTo_post [THEN iffD2, standard]
 
 
-(*** Introduction rules: Basis, Trans, Union ***)
+subsection{*Introduction rules: Basis, Trans, Union*}
 
 lemma leadsTo_imp_LeadsTo: "F : A leadsTo B ==> F : A LeadsTo B"
 apply (simp add: LeadsTo_def)
@@ -67,7 +69,7 @@
 done
 
 
-(*** Derived rules ***)
+subsection{*Derived rules*}
 
 lemma LeadsTo_UNIV [simp]: "F : A LeadsTo UNIV"
 by (simp add: LeadsTo_def)
@@ -302,7 +304,7 @@
 done
 
 
-(*** Induction rules ***)
+subsection{*Induction rules*}
 
 (** Meta or object quantifier ????? **)
 lemma LeadsTo_wf_induct:
@@ -368,7 +370,7 @@
 done
 
 
-(*** Completion: Binary and General Finite versions ***)
+subsection{*Completion: Binary and General Finite versions*}
 
 lemma Completion:
      "[| F : A LeadsTo (A' Un C);  F : A' Co (A' Un C);