1.1 --- a/doc-src/TutorialI/Advanced/document/simp.tex Thu Jan 25 11:59:52 2001 +0100
1.2 +++ b/doc-src/TutorialI/Advanced/document/simp.tex Thu Jan 25 15:31:31 2001 +0100
1.3 @@ -94,8 +94,8 @@
1.4 once they apply, they can be used forever. The simplifier is aware of this
1.5 danger and treats permutative rules by means of a special strategy, called
1.6 \bfindex{ordered rewriting}: a permutative rewrite
1.7 -rule is only applied if the term becomes ``smaller'' (with respect to a fixed
1.8 -lexicographic ordering on terms). For example, commutativity rewrites
1.9 +rule is only applied if the term becomes smaller with respect to a fixed
1.10 +lexicographic ordering on terms. For example, commutativity rewrites
1.11 \isa{b\ {\isacharplus}\ a} to \isa{a\ {\isacharplus}\ b}, but then stops because \isa{a\ {\isacharplus}\ b} is strictly
1.12 smaller than \isa{b\ {\isacharplus}\ a}. Permutative rewrite rules can be turned into
1.13 simplification rules in the usual manner via the \isa{simp} attribute; the
1.14 @@ -150,7 +150,7 @@
1.15 form (this will always be the case unless you have done something
1.16 strange) where each occurrence of an unknown is of the form
1.17 $\Var{f}~x@1~\dots~x@n$, where the $x@i$ are distinct bound
1.18 -variables. Thus all ``standard'' rewrite rules, where all unknowns are
1.19 +variables. Thus all ordinary rewrite rules, where all unknowns are
1.20 of base type, for example \isa{{\isacharquery}m\ {\isacharplus}\ {\isacharquery}n\ {\isacharplus}\ {\isacharquery}k\ {\isacharequal}\ {\isacharquery}m\ {\isacharplus}\ {\isacharparenleft}{\isacharquery}n\ {\isacharplus}\ {\isacharquery}k{\isacharparenright}}, are OK: if an unknown is
1.21 of base type, it cannot have any arguments. Additionally, the rule
1.22 \isa{{\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymand}\ {\isacharquery}Q\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}Q\ x{\isacharparenright}{\isacharparenright}} is also OK, in
2.1 --- a/doc-src/TutorialI/Advanced/simp.thy Thu Jan 25 11:59:52 2001 +0100
2.2 +++ b/doc-src/TutorialI/Advanced/simp.thy Thu Jan 25 15:31:31 2001 +0100
2.3 @@ -79,8 +79,8 @@
2.4 once they apply, they can be used forever. The simplifier is aware of this
2.5 danger and treats permutative rules by means of a special strategy, called
2.6 \bfindex{ordered rewriting}: a permutative rewrite
2.7 -rule is only applied if the term becomes ``smaller'' (with respect to a fixed
2.8 -lexicographic ordering on terms). For example, commutativity rewrites
2.9 +rule is only applied if the term becomes smaller with respect to a fixed
2.10 +lexicographic ordering on terms. For example, commutativity rewrites
2.11 @{term"b+a"} to @{term"a+b"}, but then stops because @{term"a+b"} is strictly
2.12 smaller than @{term"b+a"}. Permutative rewrite rules can be turned into
2.13 simplification rules in the usual manner via the @{text simp} attribute; the
2.14 @@ -131,7 +131,7 @@
2.15 form (this will always be the case unless you have done something
2.16 strange) where each occurrence of an unknown is of the form
2.17 $\Var{f}~x@1~\dots~x@n$, where the $x@i$ are distinct bound
2.18 -variables. Thus all ``standard'' rewrite rules, where all unknowns are
2.19 +variables. Thus all ordinary rewrite rules, where all unknowns are
2.20 of base type, for example @{thm add_assoc}, are OK: if an unknown is
2.21 of base type, it cannot have any arguments. Additionally, the rule
2.22 @{text"(\<forall>x. ?P x \<and> ?Q x) = ((\<forall>x. ?P x) \<and> (\<forall>x. ?Q x))"} is also OK, in
3.1 --- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy Thu Jan 25 11:59:52 2001 +0100
3.2 +++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy Thu Jan 25 15:31:31 2001 +0100
3.3 @@ -10,7 +10,7 @@
3.4 the constructs introduced above.
3.5 *}
3.6
3.7 -subsubsection{*How Can We Model Boolean Expressions?*}
3.8 +subsubsection{*Modelling Boolean Expressions*}
3.9
3.10 text{*
3.11 We want to represent boolean expressions built up from variables and
3.12 @@ -28,7 +28,7 @@
3.13 For example, the formula $P@0 \land \neg P@1$ is represented by the term
3.14 @{term"And (Var 0) (Neg(Var 1))"}.
3.15
3.16 -\subsubsection{What is the Value of a Boolean Expression?}
3.17 +\subsubsection{The Value of a Boolean Expression}
3.18
3.19 The value of a boolean expression depends on the value of its variables.
3.20 Hence the function @{text"value"} takes an additional parameter, an
3.21 @@ -66,9 +66,8 @@
3.22 else valif e env)";
3.23
3.24 text{*
3.25 -\subsubsection{Transformation Into and of If-Expressions}
3.26 +\subsubsection{Converting Boolean and If-Expressions}
3.27
3.28 -\REMARK{is this the title you wanted?}
3.29 The type @{typ"boolex"} is close to the customary representation of logical
3.30 formulae, whereas @{typ"ifex"} is designed for efficiency. It is easy to
3.31 translate from @{typ"boolex"} into @{typ"ifex"}:
4.1 --- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Thu Jan 25 11:59:52 2001 +0100
4.2 +++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Thu Jan 25 15:31:31 2001 +0100
4.3 @@ -12,7 +12,7 @@
4.4 the constructs introduced above.%
4.5 \end{isamarkuptext}%
4.6 %
4.7 -\isamarkupsubsubsection{How Can We Model Boolean Expressions?%
4.8 +\isamarkupsubsubsection{Modelling Boolean Expressions%
4.9 }
4.10 %
4.11 \begin{isamarkuptext}%
4.12 @@ -30,7 +30,7 @@
4.13 For example, the formula $P@0 \land \neg P@1$ is represented by the term
4.14 \isa{And\ {\isacharparenleft}Var\ {\isadigit{0}}{\isacharparenright}\ {\isacharparenleft}Neg\ {\isacharparenleft}Var\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}}.
4.15
4.16 -\subsubsection{What is the Value of a Boolean Expression?}
4.17 +\subsubsection{The Value of a Boolean Expression}
4.18
4.19 The value of a boolean expression depends on the value of its variables.
4.20 Hence the function \isa{value} takes an additional parameter, an
4.21 @@ -64,9 +64,8 @@
4.22 {\isachardoublequote}valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}if\ valif\ b\ env\ then\ valif\ t\ env\isanewline
4.23 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ valif\ e\ env{\isacharparenright}{\isachardoublequote}%
4.24 \begin{isamarkuptext}%
4.25 -\subsubsection{Transformation Into and of If-Expressions}
4.26 +\subsubsection{Converting Boolean and If-Expressions}
4.27
4.28 -\REMARK{is this the title you wanted?}
4.29 The type \isa{boolex} is close to the customary representation of logical
4.30 formulae, whereas \isa{ifex} is designed for efficiency. It is easy to
4.31 translate from \isa{boolex} into \isa{ifex}:%
5.1 --- a/doc-src/TutorialI/Inductive/advanced-examples.tex Thu Jan 25 11:59:52 2001 +0100
5.2 +++ b/doc-src/TutorialI/Inductive/advanced-examples.tex Thu Jan 25 15:31:31 2001 +0100
5.3 @@ -137,7 +137,7 @@
5.4 Applying this as an elimination rule yields one case where \isa{even.cases}
5.5 would yield two. Rule inversion works well when the conclusions of the
5.6 introduction rules involve datatype constructors like \isa{Suc} and \isa{\#}
5.7 -(list `cons'); freeness reasoning discards all but one or two cases.
5.8 +(list ``cons''); freeness reasoning discards all but one or two cases.
5.9
5.10 In the \isacommand{inductive\_cases} command we supplied an
5.11 attribute, \isa{elim!}, indicating that this elimination rule can be applied
6.1 --- a/doc-src/TutorialI/IsaMakefile Thu Jan 25 11:59:52 2001 +0100
6.2 +++ b/doc-src/TutorialI/IsaMakefile Thu Jan 25 15:31:31 2001 +0100
6.3 @@ -165,7 +165,7 @@
6.4 $(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \
6.5 Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/Option2.thy \
6.6 Misc/types.thy Misc/prime_def.thy Misc/case_exprs.thy \
6.7 - Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy
6.8 + Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy Misc/appendix.thy
6.9 $(USEDIR) Misc
6.10 @rm -f tutorial.dvi
6.11
7.1 --- a/doc-src/TutorialI/Misc/ROOT.ML Thu Jan 25 11:59:52 2001 +0100
7.2 +++ b/doc-src/TutorialI/Misc/ROOT.ML Thu Jan 25 15:31:31 2001 +0100
7.3 @@ -11,3 +11,4 @@
7.4 use_thy "simp";
7.5 use_thy "Itrev";
7.6 use_thy "AdvancedInd";
7.7 +use_thy "appendix";
8.1 --- a/doc-src/TutorialI/Misc/document/natsum.tex Thu Jan 25 11:59:52 2001 +0100
8.2 +++ b/doc-src/TutorialI/Misc/document/natsum.tex Thu Jan 25 15:31:31 2001 +0100
8.3 @@ -43,8 +43,8 @@
8.4 \ttindexboldpos{\mystar}{$HOL2arithfun}, \isaindexbold{min},
8.5 \isaindexbold{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and
8.6 \ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available
8.7 - not just for natural numbers but at other types as well (see
8.8 - \S\ref{sec:overloading}). For example, given the goal \isa{x\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ x},
8.9 + not just for natural numbers but at other types as well.
8.10 + For example, given the goal \isa{x\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ x},
8.11 there is nothing to indicate that you are talking about natural numbers.
8.12 Hence Isabelle can only infer that \isa{x} is of some arbitrary type where
8.13 \isa{{\isadigit{0}}} and \isa{{\isacharplus}} are declared. As a consequence, you will be unable
8.14 @@ -54,6 +54,10 @@
8.15 \isa{x{\isacharplus}{\isadigit{0}}\ {\isacharequal}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}}. If there is enough contextual information this
8.16 may not be necessary: \isa{Suc\ x\ {\isacharequal}\ x} automatically implies
8.17 \isa{x{\isacharcolon}{\isacharcolon}nat} because \isa{Suc} is not overloaded.
8.18 +
8.19 + For details see \S\ref{sec:numbers} and \S\ref{sec:overloading};
8.20 + Table~\ref{tab:overloading} in the appendix shows the most important overloaded
8.21 + operations.
8.22 \end{warn}
8.23
8.24 Simple arithmetic goals are proved automatically by both \isa{auto} and the
9.1 --- a/doc-src/TutorialI/Misc/natsum.thy Thu Jan 25 11:59:52 2001 +0100
9.2 +++ b/doc-src/TutorialI/Misc/natsum.thy Thu Jan 25 15:31:31 2001 +0100
9.3 @@ -41,8 +41,8 @@
9.4 \ttindexboldpos{\mystar}{$HOL2arithfun}, \isaindexbold{min},
9.5 \isaindexbold{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and
9.6 \ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available
9.7 - not just for natural numbers but at other types as well (see
9.8 - \S\ref{sec:overloading}). For example, given the goal @{prop"x+0 = x"},
9.9 + not just for natural numbers but at other types as well.
9.10 + For example, given the goal @{prop"x+0 = x"},
9.11 there is nothing to indicate that you are talking about natural numbers.
9.12 Hence Isabelle can only infer that @{term x} is of some arbitrary type where
9.13 @{term 0} and @{text"+"} are declared. As a consequence, you will be unable
9.14 @@ -52,6 +52,10 @@
9.15 @{text"x+0 = (x::nat)"}. If there is enough contextual information this
9.16 may not be necessary: @{prop"Suc x = x"} automatically implies
9.17 @{text"x::nat"} because @{term Suc} is not overloaded.
9.18 +
9.19 + For details see \S\ref{sec:numbers} and \S\ref{sec:overloading};
9.20 + Table~\ref{tab:overloading} in the appendix shows the most important overloaded
9.21 + operations.
9.22 \end{warn}
9.23
9.24 Simple arithmetic goals are proved automatically by both @{term auto} and the
10.1 --- a/doc-src/TutorialI/Rules/rules.tex Thu Jan 25 11:59:52 2001 +0100
10.2 +++ b/doc-src/TutorialI/Rules/rules.tex Thu Jan 25 15:31:31 2001 +0100
10.3 @@ -234,8 +234,8 @@
10.4 Recall that the conjunction elimination rules --- whose Isabelle names are
10.5 \isa{conjunct1} and \isa{conjunct2} --- simply return the first or second half
10.6 of a conjunction. Rules of this sort (where the conclusion is a subformula of a
10.7 -premise) are called \textbf{destruction} rules, by analogy with the destructor
10.8 -functions of functional programming.%
10.9 +premise) are called \textbf{destruction} rules because they take apart and destroy
10.10 +a premise.%
10.11 \footnote{This Isabelle terminology has no counterpart in standard logic texts,
10.12 although the distinction between the two forms of elimination rule is well known.
10.13 Girard \cite[page 74]{girard89}, for example, writes ``The elimination rules
10.14 @@ -365,7 +365,7 @@
10.15 conclusion.
10.16
10.17 \medskip
10.18 -\indexbold{by}
10.19 +\indexbold{*by}
10.20 The \isacommand{by} command is useful for proofs like these that use
10.21 \isa{assumption} heavily. It executes an
10.22 \isacommand{apply} command, then tries to prove all remaining subgoals using
10.23 @@ -781,7 +781,7 @@
10.24 To see how this works, let us derive a rule about reducing
10.25 the scope of a universal quantifier. In mathematical notation we write
10.26 \[ \infer{P\imp\forall x.\,Q}{\forall x.\,P\imp Q} \]
10.27 -with the proviso `$x$ not free in~$P$.' Isabelle's treatment of
10.28 +with the proviso ``$x$ not free in~$P$.'' Isabelle's treatment of
10.29 substitution makes the proviso unnecessary. The conclusion is expressed as
10.30 \isa{P\
10.31 \isasymlongrightarrow\ ({\isasymforall}x.\ Q\ x)}. No substitution for the
10.32 @@ -860,7 +860,7 @@
10.33 \isacommand{apply}\ (rename_tac\ v\ w)\isanewline
10.34 \ 1.\ \isasymAnd v\ w.\ x\ <\ y\ \isasymLongrightarrow \ P\ v\ (f\ w)
10.35 \end{isabelle}
10.36 -Recall that \isa{rule_tac}\index{rule_tac|and renaming} instantiates a
10.37 +Recall that \isa{rule_tac}\index{*rule_tac!and renaming} instantiates a
10.38 theorem with specified terms. These terms may involve the goal's bound
10.39 variables, but beware of referring to variables
10.40 like~\isa{xa}. A future change to your theories could change the set of names
10.41 @@ -1686,7 +1686,7 @@
10.42
10.43 The next step is to put
10.44 the theorem \isa{gcd_mult_0} into a simplified form, performing the steps
10.45 -$\gcd(1,n)=1$ and $k\times1=k$. The \isa{simplified}\indexbold{simplified}
10.46 +$\gcd(1,n)=1$ and $k\times1=k$. The \isaindexbold{simplified}
10.47 attribute takes a theorem
10.48 and returns the result of simplifying it, with respect to the default
10.49 simplification rules:
10.50 @@ -1769,7 +1769,7 @@
10.51 \end{isabelle}
10.52
10.53 \medskip
10.54 -The \isa{rule_format}\indexbold{rule_format} directive replaces a common usage
10.55 +The \isaindexbold{rule_format} directive replaces a common usage
10.56 of \isa{THEN}\@. It is needed in proofs by induction when the induction formula must be
10.57 expressed using
10.58 \isa{\isasymlongrightarrow} and \isa{\isasymforall}. For example, in
11.1 --- a/doc-src/TutorialI/Sets/sets.tex Thu Jan 25 11:59:52 2001 +0100
11.2 +++ b/doc-src/TutorialI/Sets/sets.tex Thu Jan 25 15:31:31 2001 +0100
11.3 @@ -871,7 +871,7 @@
11.4 Many familiar induction principles are instances of this rule.
11.5 For example, the predecessor relation on the natural numbers
11.6 is well-founded; induction over it is mathematical induction.
11.7 -The `tail of' relation on lists is well-founded; induction over
11.8 +The ``tail of'' relation on lists is well-founded; induction over
11.9 it is structural induction.
11.10
11.11 Well-foundedness can be difficult to show. The various
12.1 --- a/doc-src/TutorialI/ToyList/ToyList.thy Thu Jan 25 11:59:52 2001 +0100
12.2 +++ b/doc-src/TutorialI/ToyList/ToyList.thy Thu Jan 25 15:31:31 2001 +0100
12.3 @@ -177,7 +177,7 @@
12.4
12.5 txt{*\noindent\index{*induct_tac}%
12.6 This tells Isabelle to perform induction on variable @{term"xs"}. The suffix
12.7 -@{term"tac"} stands for ``tactic'', a synonym for ``theorem proving function''.
12.8 +@{term"tac"} stands for \bfindex{tactic}, a synonym for ``theorem proving function''.
12.9 By default, induction acts on the first subgoal. The new proof state contains
12.10 two subgoals, namely the base case (@{term[source]Nil}) and the induction step
12.11 (@{term[source]Cons}):
12.12 @@ -207,7 +207,7 @@
12.13 txt{*\noindent
12.14 This command tells Isabelle to apply a proof strategy called
12.15 @{text"auto"} to all subgoals. Essentially, @{text"auto"} tries to
12.16 -``simplify'' the subgoals. In our case, subgoal~1 is solved completely (thanks
12.17 +simplify the subgoals. In our case, subgoal~1 is solved completely (thanks
12.18 to the equation @{prop"rev [] = []"}) and disappears; the simplified version
12.19 of subgoal~2 becomes the new subgoal~1:
12.20 @{subgoals[display,indent=0,margin=70]}
13.1 --- a/doc-src/TutorialI/ToyList/document/ToyList.tex Thu Jan 25 11:59:52 2001 +0100
13.2 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Thu Jan 25 15:31:31 2001 +0100
13.3 @@ -172,7 +172,7 @@
13.4 \begin{isamarkuptxt}%
13.5 \noindent\index{*induct_tac}%
13.6 This tells Isabelle to perform induction on variable \isa{xs}. The suffix
13.7 -\isa{tac} stands for ``tactic'', a synonym for ``theorem proving function''.
13.8 +\isa{tac} stands for \bfindex{tactic}, a synonym for ``theorem proving function''.
13.9 By default, induction acts on the first subgoal. The new proof state contains
13.10 two subgoals, namely the base case (\isa{Nil}) and the induction step
13.11 (\isa{Cons}):
13.12 @@ -204,7 +204,7 @@
13.13 \noindent
13.14 This command tells Isabelle to apply a proof strategy called
13.15 \isa{auto} to all subgoals. Essentially, \isa{auto} tries to
13.16 -``simplify'' the subgoals. In our case, subgoal~1 is solved completely (thanks
13.17 +simplify the subgoals. In our case, subgoal~1 is solved completely (thanks
13.18 to the equation \isa{rev\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}) and disappears; the simplified version
13.19 of subgoal~2 becomes the new subgoal~1:
13.20 \begin{isabelle}%
14.1 --- a/doc-src/TutorialI/Trie/Trie.thy Thu Jan 25 11:59:52 2001 +0100
14.2 +++ b/doc-src/TutorialI/Trie/Trie.thy Thu Jan 25 15:31:31 2001 +0100
14.3 @@ -132,7 +132,7 @@
14.4 proof states are invisible, and we rely on the (possibly brittle) magic of
14.5 @{text auto} (@{text simp_all} will not do --- try it) to split the subgoals
14.6 of the induction up in such a way that case distinction on @{term bs} makes
14.7 -sense and solves the proof. Part~\ref{Isar} shows you how to write readable
14.8 +sense and solves the proof. Chapter~\ref{ch:Isar} shows you how to write readable
14.9 and stable proofs.
14.10 *};
14.11
15.1 --- a/doc-src/TutorialI/Trie/document/Trie.tex Thu Jan 25 11:59:52 2001 +0100
15.2 +++ b/doc-src/TutorialI/Trie/document/Trie.tex Thu Jan 25 15:31:31 2001 +0100
15.3 @@ -122,7 +122,7 @@
15.4 proof states are invisible, and we rely on the (possibly brittle) magic of
15.5 \isa{auto} (\isa{simp{\isacharunderscore}all} will not do --- try it) to split the subgoals
15.6 of the induction up in such a way that case distinction on \isa{bs} makes
15.7 -sense and solves the proof. Part~\ref{Isar} shows you how to write readable
15.8 +sense and solves the proof. Chapter~\ref{ch:Isar} shows you how to write readable
15.9 and stable proofs.%
15.10 \end{isamarkuptext}%
15.11 \end{isabellebody}%
16.1 --- a/doc-src/TutorialI/Types/Overloading2.thy Thu Jan 25 11:59:52 2001 +0100
16.2 +++ b/doc-src/TutorialI/Types/Overloading2.thy Thu Jan 25 15:31:31 2001 +0100
16.3 @@ -22,38 +22,10 @@
16.4
16.5 text{*
16.6 HOL comes with a number of overloaded constants and corresponding classes.
16.7 -The most important ones are listed in Table~\ref{tab:overloading}. They are
16.8 +The most important ones are listed in Table~\ref{tab:overloading} in the appendix. They are
16.9 defined on all numeric types and sometimes on other types as well, for example
16.10 @{text"-"}, @{text"\<le>"} and @{text"<"} on sets.
16.11
16.12 -\begin{table}[htbp]
16.13 -\begin{center}
16.14 -\begin{tabular}{lll}
16.15 -Constant & Type & Syntax \\
16.16 -\hline
16.17 -@{term 0} & @{text "'a::zero"} \\
16.18 -@{text"+"} & @{text "('a::plus) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 65) \\
16.19 -@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 65) \\
16.20 -@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a"} \\
16.21 -@{text"*"} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
16.22 -@{text div} & @{text "('a::div) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
16.23 -@{text mod} & @{text "('a::div) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
16.24 -@{text dvd} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
16.25 -@{text"/"} & @{text "('a::inverse) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
16.26 -@{text"^"} & @{text "('a::power) \<Rightarrow> nat \<Rightarrow> 'a"} & (infixr 80) \\
16.27 -@{term abs} & @{text "('a::minus) \<Rightarrow> 'a"} & ${\mid} x {\mid}$\\
16.28 -@{text"\<le>"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
16.29 -@{text"<"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
16.30 -@{term min} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\
16.31 -@{term max} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\
16.32 -@{term Least} & @{text "('a::ord \<Rightarrow> bool) \<Rightarrow> 'a"} &
16.33 -@{text LEAST}$~x.~P$
16.34 -\end{tabular}
16.35 -\caption{Overloaded Constants in HOL}
16.36 -\label{tab:overloading}
16.37 -\end{center}
16.38 -\end{table}
16.39 -
16.40 In addition there is a special input syntax for bounded quantifiers:
16.41 \begin{center}
16.42 \begin{tabular}{lcl}
17.1 --- a/doc-src/TutorialI/Types/document/Overloading2.tex Thu Jan 25 11:59:52 2001 +0100
17.2 +++ b/doc-src/TutorialI/Types/document/Overloading2.tex Thu Jan 25 15:31:31 2001 +0100
17.3 @@ -24,38 +24,10 @@
17.4 %
17.5 \begin{isamarkuptext}%
17.6 HOL comes with a number of overloaded constants and corresponding classes.
17.7 -The most important ones are listed in Table~\ref{tab:overloading}. They are
17.8 +The most important ones are listed in Table~\ref{tab:overloading} in the appendix. They are
17.9 defined on all numeric types and sometimes on other types as well, for example
17.10 \isa{{\isacharminus}}, \isa{{\isasymle}} and \isa{{\isacharless}} on sets.
17.11
17.12 -\begin{table}[htbp]
17.13 -\begin{center}
17.14 -\begin{tabular}{lll}
17.15 -Constant & Type & Syntax \\
17.16 -\hline
17.17 -\isa{{\isadigit{0}}} & \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}zero} \\
17.18 -\isa{{\isacharplus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}plus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 65) \\
17.19 -\isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 65) \\
17.20 -\isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} \\
17.21 -\isa{{\isacharasterisk}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}times{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
17.22 -\isa{div} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}div{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
17.23 -\isa{mod} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}div{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
17.24 -\isa{dvd} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}times{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
17.25 -\isa{{\isacharslash}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}inverse{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
17.26 -\isa{{\isacharcircum}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}power{\isacharparenright}\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a} & (infixr 80) \\
17.27 -\isa{abs} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} & ${\mid} x {\mid}$\\
17.28 -\isa{{\isasymle}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
17.29 -\isa{{\isacharless}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
17.30 -\isa{min} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\
17.31 -\isa{max} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\
17.32 -\isa{Least} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} &
17.33 -\isa{LEAST}$~x.~P$
17.34 -\end{tabular}
17.35 -\caption{Overloaded Constants in HOL}
17.36 -\label{tab:overloading}
17.37 -\end{center}
17.38 -\end{table}
17.39 -
17.40 In addition there is a special input syntax for bounded quantifiers:
17.41 \begin{center}
17.42 \begin{tabular}{lcl}
18.1 --- a/doc-src/TutorialI/Types/numerics.tex Thu Jan 25 11:59:52 2001 +0100
18.2 +++ b/doc-src/TutorialI/Types/numerics.tex Thu Jan 25 15:31:31 2001 +0100
18.3 @@ -6,7 +6,10 @@
18.4 \isa{int} of \textbf{integers}, which lack induction but support true
18.5 subtraction. The logic HOL-Real also has the type \isa{real} of real
18.6 numbers. Isabelle has no subtyping, so the numeric types are distinct and
18.7 -there are functions to convert between them.
18.8 +there are functions to convert between them. Fortunately most numeric
18.9 +operations are overloaded: the same symbol can be used at all numeric types.
18.10 +Table~\ref{tab:overloading} in the appendix shows the most important operations,
18.11 +together with the priorities of the infix symbols.
18.12
18.13 The integers are preferable to the natural numbers for reasoning about
18.14 complicated arithmetic expressions. For example, a termination proof
19.1 --- a/doc-src/TutorialI/appendix.tex Thu Jan 25 11:59:52 2001 +0100
19.2 +++ b/doc-src/TutorialI/appendix.tex Thu Jan 25 15:31:31 2001 +0100
19.3 @@ -3,7 +3,7 @@
19.4 \chapter{Appendix}
19.5 \label{sec:Appendix}
19.6
19.7 -\begin{figure}[htbp]
19.8 +\begin{table}[htbp]
19.9 \begin{center}
19.10 \begin{tabular}{|l|l|l|}
19.11 \hline
19.12 @@ -98,11 +98,13 @@
19.13 \hline
19.14 \end{tabular}
19.15 \end{center}
19.16 -\caption{Mathematical symbols, their ASCII-equivalents and ProofGeneral codes}
19.17 -\label{fig:ascii}
19.18 -\end{figure}\indexbold{ASCII symbols}
19.19 +\caption{Mathematical symbols, their ASCII-equivalents and X-Symbol codes}
19.20 +\label{tab:ascii}
19.21 +\end{table}\indexbold{ASCII symbols}
19.22
19.23 -\begin{figure}[htbp]
19.24 +\input{Misc/document/appendix.tex}
19.25 +
19.26 +\begin{table}[htbp]
19.27 \begin{center}
19.28 \begin{tabular}{|lllllllll|}
19.29 \hline
19.30 @@ -143,11 +145,11 @@
19.31 \end{tabular}
19.32 \end{center}
19.33 \caption{Reserved words in HOL terms}
19.34 -\label{fig:ReservedWords}
19.35 -\end{figure}
19.36 +\label{tab:ReservedWords}
19.37 +\end{table}
19.38
19.39
19.40 -%\begin{figure}[htbp]
19.41 +%\begin{table}[htbp]
19.42 %\begin{center}
19.43 %\begin{tabular}{|lllll|}
19.44 %\hline
19.45 @@ -175,5 +177,5 @@
19.46 %\end{tabular}
19.47 %\end{center}
19.48 %\caption{Minor keywords in HOL theories}
19.49 -%\label{fig:keywords}
19.50 -%\end{figure}
19.51 +%\label{tab:keywords}
19.52 +%\end{table}
20.1 --- a/doc-src/TutorialI/basics.tex Thu Jan 25 11:59:52 2001 +0100
20.2 +++ b/doc-src/TutorialI/basics.tex Thu Jan 25 15:31:31 2001 +0100
20.3 @@ -62,7 +62,7 @@
20.4
20.5 HOL's theory collection is available online at
20.6 \begin{center}\small
20.7 - \url{http://isabelle.in.tum.de/library/}
20.8 + \url{http://isabelle.in.tum.de/library/HOL/}
20.9 \end{center}
20.10 and is recommended browsing. Note that most of the theories
20.11 are based on classical Isabelle without the Isar extension. This means that
20.12 @@ -233,7 +233,7 @@
20.13 \end{itemize}
20.14
20.15 For the sake of readability the usual mathematical symbols are used throughout
20.16 -the tutorial. Their ASCII-equivalents are shown in figure~\ref{fig:ascii} in
20.17 +the tutorial. Their ASCII-equivalents are shown in table~\ref{tab:ascii} in
20.18 the appendix.
20.19
20.20
20.21 @@ -279,7 +279,7 @@
20.22
20.23 Some interfaces (including the shell level) offer special fonts with
20.24 mathematical symbols. For those that do not, remember that ASCII-equivalents
20.25 -are shown in figure~\ref{fig:ascii} in the appendix.
20.26 +are shown in table~\ref{tab:ascii} in the appendix.
20.27
20.28 Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}}
20.29 Commands may but need not be terminated by semicolons.
21.1 --- a/doc-src/TutorialI/fp.tex Thu Jan 25 11:59:52 2001 +0100
21.2 +++ b/doc-src/TutorialI/fp.tex Thu Jan 25 15:31:31 2001 +0100
21.3 @@ -129,10 +129,10 @@
21.4 \isa{\isacommand{theory}~T~=~\dots~:} is processed, the
21.5 modified parent is reloaded automatically.
21.6
21.7 - The only time when you need to load a theory by hand is when you simply
21.8 - want to check if it loads successfully without wanting to make use of the
21.9 - theory itself. This you can do by typing
21.10 - \isa{\isacommand{use\_thy}\indexbold{*use_thy}~"T"}.
21.11 +% The only time when you need to load a theory by hand is when you simply
21.12 +% want to check if it loads successfully without wanting to make use of the
21.13 +% theory itself. This you can do by typing
21.14 +% \isa{\isacommand{use\_thy}\indexbold{*use_thy}~"T"}.
21.15 \end{description}
21.16 Further commands are found in the Isabelle/Isar Reference Manual.
21.17
21.18 @@ -302,7 +302,7 @@
21.19 section as well, in particular in order to understand what happened if things
21.20 do not simplify as expected.
21.21
21.22 -\subsubsection{What is Simplification?}
21.23 +\subsubsection{What is Simplification}
21.24
21.25 In its most basic form, simplification means repeated application of
21.26 equations from left to right. For example, taking the rules for \isa{\at}
22.1 --- a/doc-src/TutorialI/tutorial.tex Thu Jan 25 11:59:52 2001 +0100
22.2 +++ b/doc-src/TutorialI/tutorial.tex Thu Jan 25 15:31:31 2001 +0100
22.3 @@ -91,6 +91,7 @@
22.4 \chapter{Theory Presentation}
22.5 \chapter{Case Study: Verifying a Cryptographic Protocol}
22.6 \chapter{Structured Proofs}
22.7 +\label{ch:Isar}
22.8 %\chapter{Case Study: UNIX File-System Security}
22.9 %\chapter{The Tricks of the Trade}
22.10 \input{appendix}