# HG changeset patch
# User paulson
# Date 1026248726 -7200
# Node ID 703de709a64b73ae7a8ab23f9250dfff1ab680c5
# Parent  be7105a066d35052938cd45c030f3fb1ef128677
better document preparation

diff -r be7105a066d3 -r 703de709a64b src/ZF/AC.thy
--- a/src/ZF/AC.thy	Tue Jul 09 23:03:21 2002 +0200
+++ b/src/ZF/AC.thy	Tue Jul 09 23:05:26 2002 +0200
@@ -3,13 +3,13 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
-The Axiom of Choice
+*)
 
-This definition comes from Halmos (1960), page 59.
-*)
+header{*The Axiom of Choice*}
 
 theory AC = Main:
 
+text{*This definition comes from Halmos (1960), page 59.*}
 axioms AC: "[| a: A;  !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)"
 
 (*The same as AC, but no premise a \<in> A*)
diff -r be7105a066d3 -r 703de709a64b src/ZF/Arith.thy
--- a/src/ZF/Arith.thy	Tue Jul 09 23:03:21 2002 +0200
+++ b/src/ZF/Arith.thy	Tue Jul 09 23:05:26 2002 +0200
@@ -3,9 +3,6 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
-Arithmetic operators and their definitions
-
-Proofs about elementary arithmetic: addition, multiplication, etc.
 *)
 
 (*"Difference" is subtraction of natural numbers.
@@ -14,8 +11,12 @@
   Also, rec(m, 0, %z w.z) is pred(m).   
 *)
 
+header{*Arithmetic Operators and Their Definitions*} 
+
 theory Arith = Univ:
 
+text{*Proofs about elementary arithmetic: addition, multiplication, etc.*}
+
 constdefs
   pred   :: "i=>i"    (*inverse of succ*)
     "pred(y) == THE x. y = succ(x)"
diff -r be7105a066d3 -r 703de709a64b src/ZF/ArithSimp.thy
--- a/src/ZF/ArithSimp.thy	Tue Jul 09 23:03:21 2002 +0200
+++ b/src/ZF/ArithSimp.thy	Tue Jul 09 23:05:26 2002 +0200
@@ -3,9 +3,10 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   2000  University of Cambridge
 
-Arithmetic with simplification
 *)
 
+header{*Arithmetic with simplification*}
+
 theory ArithSimp = Arith
 files "arith_data.ML":
 
diff -r be7105a066d3 -r 703de709a64b src/ZF/Bool.thy
--- a/src/ZF/Bool.thy	Tue Jul 09 23:03:21 2002 +0200
+++ b/src/ZF/Bool.thy	Tue Jul 09 23:05:26 2002 +0200
@@ -3,10 +3,9 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
-Booleans in Zermelo-Fraenkel Set Theory 
+*)
 
-2 is equal to bool, but serves a different purpose
-*)
+header{*Booleans in Zermelo-Fraenkel Set Theory*}
 
 theory Bool = pair:
 
@@ -18,6 +17,8 @@
    "1"  == "succ(0)"
    "2"  == "succ(1)"
 
+text{*2 is equal to bool, but is used as a number rather than a type.*}
+
 constdefs
   bool        :: i
     "bool == {0,1}"
diff -r be7105a066d3 -r 703de709a64b src/ZF/Cardinal.thy
--- a/src/ZF/Cardinal.thy	Tue Jul 09 23:03:21 2002 +0200
+++ b/src/ZF/Cardinal.thy	Tue Jul 09 23:05:26 2002 +0200
@@ -3,10 +3,9 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
-Cardinals in Zermelo-Fraenkel Set Theory 
+*)
 
-This theory does NOT assume the Axiom of Choice
-*)
+header{*Cardinal Numbers Without the Axiom of Choice*}
 
 theory Cardinal = OrderType + Finite + Nat + Sum:
 
diff -r be7105a066d3 -r 703de709a64b src/ZF/CardinalArith.thy
--- a/src/ZF/CardinalArith.thy	Tue Jul 09 23:03:21 2002 +0200
+++ b/src/ZF/CardinalArith.thy	Tue Jul 09 23:05:26 2002 +0200
@@ -3,13 +3,9 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
-Cardinal arithmetic -- WITHOUT the Axiom of Choice
+*)
 
-Note: Could omit proving the algebraic laws for cardinal addition and
-multiplication.  On finite cardinals these operations coincide with
-addition and multiplication of natural numbers; on infinite cardinals they
-coincide with union (maximum).  Either way we get most laws for free.
-*)
+header{*Cardinal Arithmetic Without the Axiom of Choice*}
 
 theory CardinalArith = Cardinal + OrderArith + ArithSimp + Finite:
 
@@ -94,6 +90,11 @@
 
 (*** Cardinal addition ***)
 
+text{*Note: Could omit proving the algebraic laws for cardinal addition and
+multiplication.  On finite cardinals these operations coincide with
+addition and multiplication of natural numbers; on infinite cardinals they
+coincide with union (maximum).  Either way we get most laws for free.*}
+
 (** Cardinal addition is commutative **)
 
 lemma sum_commute_eqpoll: "A+B \<approx> B+A"
diff -r be7105a066d3 -r 703de709a64b src/ZF/Cardinal_AC.thy
--- a/src/ZF/Cardinal_AC.thy	Tue Jul 09 23:03:21 2002 +0200
+++ b/src/ZF/Cardinal_AC.thy	Tue Jul 09 23:05:26 2002 +0200
@@ -3,11 +3,11 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
-Cardinal Arithmetic WITH the Axiom of Choice
-
 These results help justify infinite-branching datatypes
 *)
 
+header{*Cardinal Arithmetic Using AC*}
+
 theory Cardinal_AC = CardinalArith + Zorn:
 
 (*** Strengthened versions of existing theorems about cardinals ***)
diff -r be7105a066d3 -r 703de709a64b src/ZF/Constructible/Formula.thy
--- a/src/ZF/Constructible/Formula.thy	Tue Jul 09 23:03:21 2002 +0200
+++ b/src/ZF/Constructible/Formula.thy	Tue Jul 09 23:05:26 2002 +0200
@@ -523,11 +523,6 @@
 
 subsubsection{*The subset relation*}
 
-lemma lt_length_in_nat:
-   "[|x < length(xs); xs \<in> list(A)|] ==> x \<in> nat"
-apply (frule lt_nat_in_nat, typecheck) 
-done
-
 constdefs subset_fm :: "[i,i]=>i"
     "subset_fm(x,y) == Forall(Implies(Member(0,succ(x)), Member(0,succ(y))))"
 
diff -r be7105a066d3 -r 703de709a64b src/ZF/Datatype.thy
--- a/src/ZF/Datatype.thy	Tue Jul 09 23:03:21 2002 +0200
+++ b/src/ZF/Datatype.thy	Tue Jul 09 23:05:26 2002 +0200
@@ -3,9 +3,10 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1997  University of Cambridge
 
-(Co)Datatype Definitions for Zermelo-Fraenkel Set Theory.
 *)
 
+header{*Datatype and CoDatatype Definitions*}
+
 theory Datatype = Inductive + Univ + QUniv
   files
     "Tools/datatype_package.ML"
diff -r be7105a066d3 -r 703de709a64b src/ZF/Epsilon.thy
--- a/src/ZF/Epsilon.thy	Tue Jul 09 23:03:21 2002 +0200
+++ b/src/ZF/Epsilon.thy	Tue Jul 09 23:05:26 2002 +0200
@@ -3,9 +3,10 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-Epsilon induction and recursion
 *)
 
+header{*Epsilon Induction and Recursion*}
+
 theory Epsilon = Nat + mono:
 
 constdefs
diff -r be7105a066d3 -r 703de709a64b src/ZF/Finite.thy
--- a/src/ZF/Finite.thy	Tue Jul 09 23:03:21 2002 +0200
+++ b/src/ZF/Finite.thy	Tue Jul 09 23:05:26 2002 +0200
@@ -3,13 +3,13 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
-Finite powerset operator; finite function space
-
 prove X:Fin(A) ==> |X| < nat
 
 prove:  b: Fin(A) ==> inj(b,b) <= surj(b,b)
 *)
 
+header{*Finite Powerset Operator and Finite Function Space*}
+
 theory Finite = Inductive + Epsilon + Nat:
 
 (*The natural numbers as a datatype*)