diff -r d19cdbd8b559 -r c9cfe1638bf2 src/ZF/QPair.thy
--- a/src/ZF/QPair.thy	Sun Jul 14 15:11:21 2002 +0200
+++ b/src/ZF/QPair.thy	Sun Jul 14 15:14:43 2002 +0200
@@ -3,21 +3,24 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-Quine-inspired ordered pairs and disjoint sums, for non-well-founded data
-structures in ZF.  Does not precisely follow Quine's construction.  Thanks
-to Thomas Forster for suggesting this approach!
-
-W. V. Quine, On Ordered Pairs and Relations, in Selected Logic Papers,
-1966.
-
 Many proofs are borrowed from pair.thy and sum.thy
 
 Do we EVER have rank(a) < rank(<a;b>) ?  Perhaps if the latter rank
     is not a limit ordinal? 
 *)
 
+header{*Quine-Inspired Ordered Pairs and Disjoint Sums*}
+
 theory QPair = Sum + mono:
 
+text{*For non-well-founded data
+structures in ZF.  Does not precisely follow Quine's construction.  Thanks
+to Thomas Forster for suggesting this approach!
+
+W. V. Quine, On Ordered Pairs and Relations, in Selected Logic Papers,
+1966.
+*}
+
 constdefs
   QPair     :: "[i, i] => i"                      ("<(_;/ _)>")
     "<a;b> == a+b"
@@ -62,7 +65,7 @@
 print_translation {* [("QSigma", dependent_tr' ("@QSUM", "op <*>"))] *}
 
 
-(**** Quine ordered pairing ****)
+subsection{*Quine ordered pairing*}
 
 (** Lemmas for showing that <a;b> uniquely determines a and b **)
 
@@ -83,8 +86,8 @@
 by blast
 
 
-(*** QSigma: Disjoint union of a family of sets
-     Generalizes Cartesian product ***)
+subsubsection{*QSigma: Disjoint union of a family of sets
+     Generalizes Cartesian product*}
 
 lemma QSigmaI [intro!]: "[| a:A;  b:B(a) |] ==> <a;b> : QSigma(A,B)"
 by (simp add: QSigma_def)
@@ -95,8 +98,7 @@
     "[| c: QSigma(A,B);   
         !!x y.[| x:A;  y:B(x);  c=<x;y> |] ==> P  
      |] ==> P"
-apply (simp add: QSigma_def, blast) 
-done
+by (simp add: QSigma_def, blast) 
 
 (** Elimination rules for <a;b>:A*B -- introducing no eigenvariables **)
 
@@ -104,8 +106,7 @@
     "[| c: QSigma(A,B);   
         !!x y.[| x:A;  y:B(x);  c=<x;y> |] ==> P  
      |] ==> P"
-apply (simp add: QSigma_def, blast) 
-done
+by (simp add: QSigma_def, blast) 
 
 lemma QSigmaE2 [elim!]:
     "[| <a;b>: QSigma(A,B); [| a:A;  b:B(a) |] ==> P |] ==> P"
@@ -129,7 +130,7 @@
 by blast
 
 
-(*** Projections: qfst, qsnd ***)
+subsubsection{*Projections: qfst, qsnd*}
 
 lemma qfst_conv [simp]: "qfst(<a;b>) = a"
 by (simp add: qfst_def, blast)
@@ -147,7 +148,7 @@
 by auto
 
 
-(*** Eliminator - qsplit ***)
+subsubsection{*Eliminator: qsplit*}
 
 (*A META-equality, so that it applies to higher types as well...*)
 lemma qsplit [simp]: "qsplit(%x y. c(x,y), <a;b>) == c(a,b)"
@@ -166,7 +167,7 @@
 done
 
 
-(*** qsplit for predicates: result type o ***)
+subsubsection{*qsplit for predicates: result type o*}
 
 lemma qsplitI: "R(a,b) ==> qsplit(R, <a;b>)"
 by (simp add: qsplit_def)
@@ -176,14 +177,13 @@
     "[| qsplit(R,z);  z:QSigma(A,B);                     
         !!x y. [| z = <x;y>;  R(x,y) |] ==> P            
     |] ==> P"
-apply (simp add: qsplit_def, auto) 
-done
+by (simp add: qsplit_def, auto) 
 
 lemma qsplitD: "qsplit(R,<a;b>) ==> R(a,b)"
 by (simp add: qsplit_def)
 
 
-(*** qconverse ***)
+subsubsection{*qconverse*}
 
 lemma qconverseI [intro!]: "<a;b>:r ==> <b;a>:qconverse(r)"
 by (simp add: qconverse_def, blast)
@@ -195,8 +195,7 @@
     "[| yx : qconverse(r);   
         !!x y. [| yx=<y;x>;  <x;y>:r |] ==> P  
      |] ==> P"
-apply (simp add: qconverse_def, blast) 
-done
+by (simp add: qconverse_def, blast) 
 
 lemma qconverse_qconverse: "r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r"
 by blast
@@ -211,7 +210,7 @@
 by blast
 
 
-(**** The Quine-inspired notion of disjoint sum ****)
+subsection{*The Quine-inspired notion of disjoint sum*}
 
 lemmas qsum_defs = qsum_def QInl_def QInr_def qcase_def
 
@@ -230,8 +229,7 @@
         !!x. [| x:A;  u=QInl(x) |] ==> P;  
         !!y. [| y:B;  u=QInr(y) |] ==> P  
      |] ==> P"
-apply (simp add: qsum_defs, blast) 
-done
+by (simp add: qsum_defs, blast) 
 
 
 (** Injection and freeness equivalences, for rewriting **)
@@ -268,8 +266,7 @@
 
 lemma qsum_iff:
      "u: A <+> B <-> (EX x. x:A & u=QInl(x)) | (EX y. y:B & u=QInr(y))"
-apply blast
-done
+by blast
 
 lemma qsum_subset_iff: "A <+> B <= C <+> D <-> A<=C & B<=D"
 by blast
@@ -279,7 +276,7 @@
 apply blast
 done
 
-(*** Eliminator -- qcase ***)
+subsubsection{*Eliminator -- qcase*}
 
 lemma qcase_QInl [simp]: "qcase(c, d, QInl(a)) = c(a)"
 by (simp add: qsum_defs )
@@ -293,8 +290,7 @@
         !!x. x: A ==> c(x): C(QInl(x));    
         !!y. y: B ==> d(y): C(QInr(y))  
      |] ==> qcase(c,d,u) : C(u)"
-apply (simp add: qsum_defs , auto) 
-done
+by (simp add: qsum_defs , auto) 
 
 (** Rules for the Part primitive **)
 
@@ -311,7 +307,7 @@
 by blast
 
 
-(*** Monotonicity ***)
+subsubsection{*Monotonicity*}
 
 lemma QPair_mono: "[| a<=c;  b<=d |] ==> <a;b> <= <c;d>"
 by (simp add: QPair_def sum_mono)