tuned;
authorwenzelm
Sat Nov 03 01:33:54 2001 +0100 (2001-11-03)
changeset 12023d982f98e0f0d
parent 12022 9c3377b133c0
child 12024 b3661262541e
tuned;
src/FOL/document/root.tex
src/HOL/HOL.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Inductive.thy
src/HOL/Integ/IntArith.thy
src/HOL/Recdef.thy
src/HOL/Set.thy
src/HOL/Typedef.thy
src/HOL/ex/NatSum.thy
src/HOL/ex/Recdefs.thy
src/HOL/ex/document/root.tex
     1.1 --- a/src/FOL/document/root.tex	Sat Nov 03 01:33:33 2001 +0100
     1.2 +++ b/src/FOL/document/root.tex	Sat Nov 03 01:33:54 2001 +0100
     1.3 @@ -2,31 +2,21 @@
     1.4  % $Id$
     1.5  
     1.6  \documentclass[11pt,a4paper]{article}
     1.7 -\usepackage{isabelle,isabellesym,pdfsetup}
     1.8 +\usepackage{isabelle,isabellesym}
     1.9 +\usepackage{pdfsetup}
    1.10  
    1.11 -% proper setup for best-style documents
    1.12  \urlstyle{rm}
    1.13  \isabellestyle{it}
    1.14  
    1.15 -
    1.16  \begin{document}
    1.17  
    1.18 -\title{First-Order Logic}
    1.19 +\title{Isabelle/FOL --- First-Order Logic}
    1.20  \author{Larry Paulson and Markus Wenzel}
    1.21  \maketitle
    1.22  
    1.23  \tableofcontents
    1.24  
    1.25 -\parindent 0pt
    1.26 -\parskip 0.5ex
    1.27 -
    1.28 -\paragraph{Note.} This may serve as an example of initializing all the tools
    1.29 -and packages required for a reasonable working environment.  Please go
    1.30 -elsewhere to see actual applications of Isabelle!
    1.31 -
    1.32 +\parindent 0pt\parskip 0.5ex
    1.33  \input{session}
    1.34  
    1.35 -%\bibliographystyle{plain}
    1.36 -%\bibliography{root}
    1.37 -
    1.38  \end{document}
     2.1 --- a/src/HOL/HOL.thy	Sat Nov 03 01:33:33 2001 +0100
     2.2 +++ b/src/HOL/HOL.thy	Sat Nov 03 01:33:54 2001 +0100
     2.3 @@ -232,7 +232,8 @@
     2.4    thus "x == y" by (rule eq_reflection)
     2.5  qed
     2.6  
     2.7 -lemma atomize_conj [atomize]: "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)"
     2.8 +lemma atomize_conj [atomize]:
     2.9 +  "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)"
    2.10  proof
    2.11    assume "!!C. (A ==> B ==> PROP C) ==> PROP C"
    2.12    show "A & B" by (rule conjI)
     3.1 --- a/src/HOL/Hilbert_Choice.thy	Sat Nov 03 01:33:33 2001 +0100
     3.2 +++ b/src/HOL/Hilbert_Choice.thy	Sat Nov 03 01:33:54 2001 +0100
     3.3 @@ -2,9 +2,9 @@
     3.4      ID:         $Id$
     3.5      Author:     Lawrence C Paulson
     3.6      Copyright   2001  University of Cambridge
     3.7 +*)
     3.8  
     3.9 -Hilbert's epsilon-operator and everything to do with the Axiom of Choice
    3.10 -*)
    3.11 +header {* Hilbert's epsilon-operator and everything to do with the Axiom of Choice *}
    3.12  
    3.13  theory Hilbert_Choice = NatArith
    3.14  files ("Hilbert_Choice_lemmas.ML") ("meson_lemmas.ML") ("Tools/meson.ML"):
     4.1 --- a/src/HOL/Inductive.thy	Sat Nov 03 01:33:33 2001 +0100
     4.2 +++ b/src/HOL/Inductive.thy	Sat Nov 03 01:33:54 2001 +0100
     4.3 @@ -65,7 +65,7 @@
     4.4    induct_rulify2
     4.5  
     4.6  
     4.7 -subsubsection {* Inductive datatypes and primitive recursion *}
     4.8 +subsection {* Inductive datatypes and primitive recursion *}
     4.9  
    4.10  text {* Package setup. *}
    4.11  
     5.1 --- a/src/HOL/Integ/IntArith.thy	Sat Nov 03 01:33:33 2001 +0100
     5.2 +++ b/src/HOL/Integ/IntArith.thy	Sat Nov 03 01:33:54 2001 +0100
     5.3 @@ -1,6 +1,12 @@
     5.4 +
     5.5 +header {* Integer arithmetic *}
     5.6 +
     5.7  theory IntArith = Bin
     5.8  files ("int_arith1.ML") ("int_arith2.ML"):
     5.9  
    5.10 -use "int_arith1.ML"	setup int_arith_setup
    5.11 -use "int_arith2.ML"	lemmas [arith_split] = zabs_split
    5.12 +use "int_arith1.ML"
    5.13 +setup int_arith_setup
    5.14 +use "int_arith2.ML"
    5.15 +declare zabs_split [arith_split]
    5.16 +
    5.17  end
     6.1 --- a/src/HOL/Recdef.thy	Sat Nov 03 01:33:33 2001 +0100
     6.2 +++ b/src/HOL/Recdef.thy	Sat Nov 03 01:33:54 2001 +0100
     6.3 @@ -1,9 +1,9 @@
     6.4  (*  Title:      HOL/Recdef.thy
     6.5      ID:         $Id$
     6.6      Author:     Konrad Slind and Markus Wenzel, TU Muenchen
     6.7 +*)
     6.8  
     6.9 -TFL: recursive function definitions.
    6.10 -*)
    6.11 +header {* TFL: recursive function definitions *}
    6.12  
    6.13  theory Recdef = Wellfounded_Relations + Datatype
    6.14  files
    6.15 @@ -34,13 +34,13 @@
    6.16  lemma tfl_imp_trans: "(A --> B) ==> (B --> C) ==> (A --> C)"
    6.17    by blast
    6.18  
    6.19 -lemma tfl_disj_assoc: "(a \\<or> b) \\<or> c == a \\<or> (b \\<or> c)"
    6.20 +lemma tfl_disj_assoc: "(a \<or> b) \<or> c == a \<or> (b \<or> c)"
    6.21    by simp
    6.22  
    6.23 -lemma tfl_disjE: "P \\<or> Q ==> P --> R ==> Q --> R ==> R"
    6.24 +lemma tfl_disjE: "P \<or> Q ==> P --> R ==> Q --> R ==> R"
    6.25    by blast
    6.26  
    6.27 -lemma tfl_exE: "\\<exists>x. P x ==> \\<forall>x. P x --> Q ==> Q"
    6.28 +lemma tfl_exE: "\<exists>x. P x ==> \<forall>x. P x --> Q ==> Q"
    6.29    by blast
    6.30  
    6.31  use "../TFL/utils.ML"
     7.1 --- a/src/HOL/Set.thy	Sat Nov 03 01:33:33 2001 +0100
     7.2 +++ b/src/HOL/Set.thy	Sat Nov 03 01:33:54 2001 +0100
     7.3 @@ -515,7 +515,7 @@
     7.4    by (blast elim: equalityE)
     7.5  
     7.6  
     7.7 -section {* The Powerset operator -- Pow *}
     7.8 +subsubsection {* The Powerset operator -- Pow *}
     7.9  
    7.10  lemma Pow_iff [iff]: "(A : Pow B) = (A <= B)"
    7.11    by (simp add: Pow_def)
    7.12 @@ -575,7 +575,7 @@
    7.13    by (unfold Un_def) blast
    7.14  
    7.15  
    7.16 -subsection {* Binary intersection -- Int *}
    7.17 +subsubsection {* Binary intersection -- Int *}
    7.18  
    7.19  lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
    7.20    by (unfold Int_def) blast
    7.21 @@ -593,7 +593,7 @@
    7.22    by simp
    7.23  
    7.24  
    7.25 -subsection {* Set difference *}
    7.26 +subsubsection {* Set difference *}
    7.27  
    7.28  lemma Diff_iff [simp]: "(c : A - B) = (c:A & c~:B)"
    7.29    by (unfold set_diff_def) blast
    7.30 @@ -905,7 +905,7 @@
    7.31    done
    7.32  
    7.33  
    7.34 -section {* Transitivity rules for calculational reasoning *}
    7.35 +subsection {* Transitivity rules for calculational reasoning *}
    7.36  
    7.37  lemma forw_subst: "a = b ==> P b ==> P a"
    7.38    by (rule ssubst)
     8.1 --- a/src/HOL/Typedef.thy	Sat Nov 03 01:33:33 2001 +0100
     8.2 +++ b/src/HOL/Typedef.thy	Sat Nov 03 01:33:54 2001 +0100
     8.3 @@ -8,8 +8,6 @@
     8.4  theory Typedef = Set
     8.5  files ("Tools/typedef_package.ML"):
     8.6  
     8.7 -subsection {* HOL type definitions *}
     8.8 -
     8.9  constdefs
    8.10    type_definition :: "('a => 'b) => ('b => 'a) => 'b set => bool"
    8.11    "type_definition Rep Abs A ==
     9.1 --- a/src/HOL/ex/NatSum.thy	Sat Nov 03 01:33:33 2001 +0100
     9.2 +++ b/src/HOL/ex/NatSum.thy	Sat Nov 03 01:33:54 2001 +0100
     9.3 @@ -22,7 +22,7 @@
     9.4  declare diff_mult_distrib [simp] diff_mult_distrib2 [simp]
     9.5  
     9.6  text {*
     9.7 -  \medskip The sum of the first @{term n} odd numbers equals @{term n}
     9.8 +  \medskip The sum of the first @{text n} odd numbers equals @{text n}
     9.9    squared.
    9.10  *}
    9.11  
    9.12 @@ -46,7 +46,7 @@
    9.13  
    9.14  
    9.15  text {*
    9.16 -  \medskip The sum of the first @{term n} odd cubes
    9.17 +  \medskip The sum of the first @{text n} odd cubes
    9.18  *}
    9.19  
    9.20  lemma sum_of_odd_cubes:
    9.21 @@ -58,7 +58,7 @@
    9.22    done
    9.23  
    9.24  text {*
    9.25 -  \medskip The sum of the first @{term n} positive integers equals
    9.26 +  \medskip The sum of the first @{text n} positive integers equals
    9.27    @{text "n (n + 1) / 2"}.*}
    9.28  
    9.29  lemma sum_of_naturals:
    9.30 @@ -114,7 +114,7 @@
    9.31  
    9.32  
    9.33  text {*
    9.34 -  \medskip Sums of geometric series: @{term 2}, @{term 3} and the
    9.35 +  \medskip Sums of geometric series: @{text 2}, @{text 3} and the
    9.36    general case.
    9.37  *}
    9.38  
    10.1 --- a/src/HOL/ex/Recdefs.thy	Sat Nov 03 01:33:33 2001 +0100
    10.2 +++ b/src/HOL/ex/Recdefs.thy	Sat Nov 03 01:33:54 2001 +0100
    10.3 @@ -76,7 +76,7 @@
    10.4  text {*
    10.5    \medskip Not handled automatically.  Should be the predecessor
    10.6    function, but there is an unnecessary "looping" recursive call in
    10.7 -  @{term "k 1"}.
    10.8 +  @{text "k 1"}.
    10.9  *}
   10.10  
   10.11  consts k :: "nat => nat"
    11.1 --- a/src/HOL/ex/document/root.tex	Sat Nov 03 01:33:33 2001 +0100
    11.2 +++ b/src/HOL/ex/document/root.tex	Sat Nov 03 01:33:54 2001 +0100
    11.3 @@ -2,8 +2,9 @@
    11.4  % $Id$
    11.5  
    11.6  \documentclass[11pt,a4paper]{article}
    11.7 -\usepackage{isabelle,isabellesym,pdfsetup}
    11.8 +\usepackage{isabelle,isabellesym}
    11.9  \usepackage[english]{babel}
   11.10 +\usepackage{pdfsetup}
   11.11  
   11.12  \urlstyle{rm}
   11.13  \isabellestyle{it}