--- 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);