--- 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}
--- 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)
--- 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"):
--- 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. *}
--- 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
--- 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"
--- 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)
--- 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 ==
--- 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.
*}
--- 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"
--- 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}