# HG changeset patch
# User wenzelm
# Date 1004747634 -3600
# Node ID d982f98e0f0da87a2a8d9e04ab22c394e91f0fb3
# Parent  9c3377b133c06c89542112033e2a76e46882fea8
tuned;

diff -r 9c3377b133c0 -r d982f98e0f0d src/FOL/document/root.tex
--- a/src/FOL/document/root.tex	Sat Nov 03 01:33:33 2001 +0100
+++ b/src/FOL/document/root.tex	Sat Nov 03 01:33:54 2001 +0100
@@ -2,31 +2,21 @@
 % $Id$
 
 \documentclass[11pt,a4paper]{article}
-\usepackage{isabelle,isabellesym,pdfsetup}
+\usepackage{isabelle,isabellesym}
+\usepackage{pdfsetup}
 
-% proper setup for best-style documents
 \urlstyle{rm}
 \isabellestyle{it}
 
-
 \begin{document}
 
-\title{First-Order Logic}
+\title{Isabelle/FOL --- First-Order Logic}
 \author{Larry Paulson and Markus Wenzel}
 \maketitle
 
 \tableofcontents
 
-\parindent 0pt
-\parskip 0.5ex
-
-\paragraph{Note.} This may serve as an example of initializing all the tools
-and packages required for a reasonable working environment.  Please go
-elsewhere to see actual applications of Isabelle!
-
+\parindent 0pt\parskip 0.5ex
 \input{session}
 
-%\bibliographystyle{plain}
-%\bibliography{root}
-
 \end{document}
diff -r 9c3377b133c0 -r d982f98e0f0d src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat Nov 03 01:33:33 2001 +0100
+++ b/src/HOL/HOL.thy	Sat Nov 03 01:33:54 2001 +0100
@@ -232,7 +232,8 @@
   thus "x == y" by (rule eq_reflection)
 qed
 
-lemma atomize_conj [atomize]: "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)"
+lemma atomize_conj [atomize]:
+  "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)"
 proof
   assume "!!C. (A ==> B ==> PROP C) ==> PROP C"
   show "A & B" by (rule conjI)
diff -r 9c3377b133c0 -r d982f98e0f0d src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Sat Nov 03 01:33:33 2001 +0100
+++ b/src/HOL/Hilbert_Choice.thy	Sat Nov 03 01:33:54 2001 +0100
@@ -2,9 +2,9 @@
     ID:         $Id$
     Author:     Lawrence C Paulson
     Copyright   2001  University of Cambridge
+*)
 
-Hilbert's epsilon-operator and everything to do with the Axiom of Choice
-*)
+header {* Hilbert's epsilon-operator and everything to do with the Axiom of Choice *}
 
 theory Hilbert_Choice = NatArith
 files ("Hilbert_Choice_lemmas.ML") ("meson_lemmas.ML") ("Tools/meson.ML"):
diff -r 9c3377b133c0 -r d982f98e0f0d src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Sat Nov 03 01:33:33 2001 +0100
+++ b/src/HOL/Inductive.thy	Sat Nov 03 01:33:54 2001 +0100
@@ -65,7 +65,7 @@
   induct_rulify2
 
 
-subsubsection {* Inductive datatypes and primitive recursion *}
+subsection {* Inductive datatypes and primitive recursion *}
 
 text {* Package setup. *}
 
diff -r 9c3377b133c0 -r d982f98e0f0d src/HOL/Integ/IntArith.thy
--- a/src/HOL/Integ/IntArith.thy	Sat Nov 03 01:33:33 2001 +0100
+++ b/src/HOL/Integ/IntArith.thy	Sat Nov 03 01:33:54 2001 +0100
@@ -1,6 +1,12 @@
+
+header {* Integer arithmetic *}
+
 theory IntArith = Bin
 files ("int_arith1.ML") ("int_arith2.ML"):
 
-use "int_arith1.ML"	setup int_arith_setup
-use "int_arith2.ML"	lemmas [arith_split] = zabs_split
+use "int_arith1.ML"
+setup int_arith_setup
+use "int_arith2.ML"
+declare zabs_split [arith_split]
+
 end
diff -r 9c3377b133c0 -r d982f98e0f0d src/HOL/Recdef.thy
--- a/src/HOL/Recdef.thy	Sat Nov 03 01:33:33 2001 +0100
+++ b/src/HOL/Recdef.thy	Sat Nov 03 01:33:54 2001 +0100
@@ -1,9 +1,9 @@
 (*  Title:      HOL/Recdef.thy
     ID:         $Id$
     Author:     Konrad Slind and Markus Wenzel, TU Muenchen
+*)
 
-TFL: recursive function definitions.
-*)
+header {* TFL: recursive function definitions *}
 
 theory Recdef = Wellfounded_Relations + Datatype
 files
@@ -34,13 +34,13 @@
 lemma tfl_imp_trans: "(A --> B) ==> (B --> C) ==> (A --> C)"
   by blast
 
-lemma tfl_disj_assoc: "(a \\<or> b) \\<or> c == a \\<or> (b \\<or> c)"
+lemma tfl_disj_assoc: "(a \<or> b) \<or> c == a \<or> (b \<or> c)"
   by simp
 
-lemma tfl_disjE: "P \\<or> Q ==> P --> R ==> Q --> R ==> R"
+lemma tfl_disjE: "P \<or> Q ==> P --> R ==> Q --> R ==> R"
   by blast
 
-lemma tfl_exE: "\\<exists>x. P x ==> \\<forall>x. P x --> Q ==> Q"
+lemma tfl_exE: "\<exists>x. P x ==> \<forall>x. P x --> Q ==> Q"
   by blast
 
 use "../TFL/utils.ML"
diff -r 9c3377b133c0 -r d982f98e0f0d src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sat Nov 03 01:33:33 2001 +0100
+++ b/src/HOL/Set.thy	Sat Nov 03 01:33:54 2001 +0100
@@ -515,7 +515,7 @@
   by (blast elim: equalityE)
 
 
-section {* The Powerset operator -- Pow *}
+subsubsection {* The Powerset operator -- Pow *}
 
 lemma Pow_iff [iff]: "(A : Pow B) = (A <= B)"
   by (simp add: Pow_def)
@@ -575,7 +575,7 @@
   by (unfold Un_def) blast
 
 
-subsection {* Binary intersection -- Int *}
+subsubsection {* Binary intersection -- Int *}
 
 lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
   by (unfold Int_def) blast
@@ -593,7 +593,7 @@
   by simp
 
 
-subsection {* Set difference *}
+subsubsection {* Set difference *}
 
 lemma Diff_iff [simp]: "(c : A - B) = (c:A & c~:B)"
   by (unfold set_diff_def) blast
@@ -905,7 +905,7 @@
   done
 
 
-section {* Transitivity rules for calculational reasoning *}
+subsection {* Transitivity rules for calculational reasoning *}
 
 lemma forw_subst: "a = b ==> P b ==> P a"
   by (rule ssubst)
diff -r 9c3377b133c0 -r d982f98e0f0d src/HOL/Typedef.thy
--- a/src/HOL/Typedef.thy	Sat Nov 03 01:33:33 2001 +0100
+++ b/src/HOL/Typedef.thy	Sat Nov 03 01:33:54 2001 +0100
@@ -8,8 +8,6 @@
 theory Typedef = Set
 files ("Tools/typedef_package.ML"):
 
-subsection {* HOL type definitions *}
-
 constdefs
   type_definition :: "('a => 'b) => ('b => 'a) => 'b set => bool"
   "type_definition Rep Abs A ==
diff -r 9c3377b133c0 -r d982f98e0f0d src/HOL/ex/NatSum.thy
--- a/src/HOL/ex/NatSum.thy	Sat Nov 03 01:33:33 2001 +0100
+++ b/src/HOL/ex/NatSum.thy	Sat Nov 03 01:33:54 2001 +0100
@@ -22,7 +22,7 @@
 declare diff_mult_distrib [simp] diff_mult_distrib2 [simp]
 
 text {*
-  \medskip The sum of the first @{term n} odd numbers equals @{term n}
+  \medskip The sum of the first @{text n} odd numbers equals @{text n}
   squared.
 *}
 
@@ -46,7 +46,7 @@
 
 
 text {*
-  \medskip The sum of the first @{term n} odd cubes
+  \medskip The sum of the first @{text n} odd cubes
 *}
 
 lemma sum_of_odd_cubes:
@@ -58,7 +58,7 @@
   done
 
 text {*
-  \medskip The sum of the first @{term n} positive integers equals
+  \medskip The sum of the first @{text n} positive integers equals
   @{text "n (n + 1) / 2"}.*}
 
 lemma sum_of_naturals:
@@ -114,7 +114,7 @@
 
 
 text {*
-  \medskip Sums of geometric series: @{term 2}, @{term 3} and the
+  \medskip Sums of geometric series: @{text 2}, @{text 3} and the
   general case.
 *}
 
diff -r 9c3377b133c0 -r d982f98e0f0d src/HOL/ex/Recdefs.thy
--- a/src/HOL/ex/Recdefs.thy	Sat Nov 03 01:33:33 2001 +0100
+++ b/src/HOL/ex/Recdefs.thy	Sat Nov 03 01:33:54 2001 +0100
@@ -76,7 +76,7 @@
 text {*
   \medskip Not handled automatically.  Should be the predecessor
   function, but there is an unnecessary "looping" recursive call in
-  @{term "k 1"}.
+  @{text "k 1"}.
 *}
 
 consts k :: "nat => nat"
diff -r 9c3377b133c0 -r d982f98e0f0d src/HOL/ex/document/root.tex
--- a/src/HOL/ex/document/root.tex	Sat Nov 03 01:33:33 2001 +0100
+++ b/src/HOL/ex/document/root.tex	Sat Nov 03 01:33:54 2001 +0100
@@ -2,8 +2,9 @@
 % $Id$
 
 \documentclass[11pt,a4paper]{article}
-\usepackage{isabelle,isabellesym,pdfsetup}
+\usepackage{isabelle,isabellesym}
 \usepackage[english]{babel}
+\usepackage{pdfsetup}
 
 \urlstyle{rm}
 \isabellestyle{it}