--- a/doc-src/TutorialI/Advanced/document/simp.tex Thu Jan 25 11:59:52 2001 +0100
+++ b/doc-src/TutorialI/Advanced/document/simp.tex Thu Jan 25 15:31:31 2001 +0100
@@ -94,8 +94,8 @@
once they apply, they can be used forever. The simplifier is aware of this
danger and treats permutative rules by means of a special strategy, called
\bfindex{ordered rewriting}: a permutative rewrite
-rule is only applied if the term becomes ``smaller'' (with respect to a fixed
-lexicographic ordering on terms). For example, commutativity rewrites
+rule is only applied if the term becomes smaller with respect to a fixed
+lexicographic ordering on terms. For example, commutativity rewrites
\isa{b\ {\isacharplus}\ a} to \isa{a\ {\isacharplus}\ b}, but then stops because \isa{a\ {\isacharplus}\ b} is strictly
smaller than \isa{b\ {\isacharplus}\ a}. Permutative rewrite rules can be turned into
simplification rules in the usual manner via the \isa{simp} attribute; the
@@ -150,7 +150,7 @@
form (this will always be the case unless you have done something
strange) where each occurrence of an unknown is of the form
$\Var{f}~x@1~\dots~x@n$, where the $x@i$ are distinct bound
-variables. Thus all ``standard'' rewrite rules, where all unknowns are
+variables. Thus all ordinary rewrite rules, where all unknowns are
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
of base type, it cannot have any arguments. Additionally, the rule
\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
--- a/doc-src/TutorialI/Advanced/simp.thy Thu Jan 25 11:59:52 2001 +0100
+++ b/doc-src/TutorialI/Advanced/simp.thy Thu Jan 25 15:31:31 2001 +0100
@@ -79,8 +79,8 @@
once they apply, they can be used forever. The simplifier is aware of this
danger and treats permutative rules by means of a special strategy, called
\bfindex{ordered rewriting}: a permutative rewrite
-rule is only applied if the term becomes ``smaller'' (with respect to a fixed
-lexicographic ordering on terms). For example, commutativity rewrites
+rule is only applied if the term becomes smaller with respect to a fixed
+lexicographic ordering on terms. For example, commutativity rewrites
@{term"b+a"} to @{term"a+b"}, but then stops because @{term"a+b"} is strictly
smaller than @{term"b+a"}. Permutative rewrite rules can be turned into
simplification rules in the usual manner via the @{text simp} attribute; the
@@ -131,7 +131,7 @@
form (this will always be the case unless you have done something
strange) where each occurrence of an unknown is of the form
$\Var{f}~x@1~\dots~x@n$, where the $x@i$ are distinct bound
-variables. Thus all ``standard'' rewrite rules, where all unknowns are
+variables. Thus all ordinary rewrite rules, where all unknowns are
of base type, for example @{thm add_assoc}, are OK: if an unknown is
of base type, it cannot have any arguments. Additionally, the rule
@{text"(\<forall>x. ?P x \<and> ?Q x) = ((\<forall>x. ?P x) \<and> (\<forall>x. ?Q x))"} is also OK, in
--- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy Thu Jan 25 11:59:52 2001 +0100
+++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy Thu Jan 25 15:31:31 2001 +0100
@@ -10,7 +10,7 @@
the constructs introduced above.
*}
-subsubsection{*How Can We Model Boolean Expressions?*}
+subsubsection{*Modelling Boolean Expressions*}
text{*
We want to represent boolean expressions built up from variables and
@@ -28,7 +28,7 @@
For example, the formula $P@0 \land \neg P@1$ is represented by the term
@{term"And (Var 0) (Neg(Var 1))"}.
-\subsubsection{What is the Value of a Boolean Expression?}
+\subsubsection{The Value of a Boolean Expression}
The value of a boolean expression depends on the value of its variables.
Hence the function @{text"value"} takes an additional parameter, an
@@ -66,9 +66,8 @@
else valif e env)";
text{*
-\subsubsection{Transformation Into and of If-Expressions}
+\subsubsection{Converting Boolean and If-Expressions}
-\REMARK{is this the title you wanted?}
The type @{typ"boolex"} is close to the customary representation of logical
formulae, whereas @{typ"ifex"} is designed for efficiency. It is easy to
translate from @{typ"boolex"} into @{typ"ifex"}:
--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Thu Jan 25 11:59:52 2001 +0100
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Thu Jan 25 15:31:31 2001 +0100
@@ -12,7 +12,7 @@
the constructs introduced above.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{How Can We Model Boolean Expressions?%
+\isamarkupsubsubsection{Modelling Boolean Expressions%
}
%
\begin{isamarkuptext}%
@@ -30,7 +30,7 @@
For example, the formula $P@0 \land \neg P@1$ is represented by the term
\isa{And\ {\isacharparenleft}Var\ {\isadigit{0}}{\isacharparenright}\ {\isacharparenleft}Neg\ {\isacharparenleft}Var\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}}.
-\subsubsection{What is the Value of a Boolean Expression?}
+\subsubsection{The Value of a Boolean Expression}
The value of a boolean expression depends on the value of its variables.
Hence the function \isa{value} takes an additional parameter, an
@@ -64,9 +64,8 @@
{\isachardoublequote}valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}if\ valif\ b\ env\ then\ valif\ t\ env\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ valif\ e\ env{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
-\subsubsection{Transformation Into and of If-Expressions}
+\subsubsection{Converting Boolean and If-Expressions}
-\REMARK{is this the title you wanted?}
The type \isa{boolex} is close to the customary representation of logical
formulae, whereas \isa{ifex} is designed for efficiency. It is easy to
translate from \isa{boolex} into \isa{ifex}:%
--- a/doc-src/TutorialI/Inductive/advanced-examples.tex Thu Jan 25 11:59:52 2001 +0100
+++ b/doc-src/TutorialI/Inductive/advanced-examples.tex Thu Jan 25 15:31:31 2001 +0100
@@ -137,7 +137,7 @@
Applying this as an elimination rule yields one case where \isa{even.cases}
would yield two. Rule inversion works well when the conclusions of the
introduction rules involve datatype constructors like \isa{Suc} and \isa{\#}
-(list `cons'); freeness reasoning discards all but one or two cases.
+(list ``cons''); freeness reasoning discards all but one or two cases.
In the \isacommand{inductive\_cases} command we supplied an
attribute, \isa{elim!}, indicating that this elimination rule can be applied
--- a/doc-src/TutorialI/IsaMakefile Thu Jan 25 11:59:52 2001 +0100
+++ b/doc-src/TutorialI/IsaMakefile Thu Jan 25 15:31:31 2001 +0100
@@ -165,7 +165,7 @@
$(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \
Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/Option2.thy \
Misc/types.thy Misc/prime_def.thy Misc/case_exprs.thy \
- Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy
+ Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy Misc/appendix.thy
$(USEDIR) Misc
@rm -f tutorial.dvi
--- a/doc-src/TutorialI/Misc/ROOT.ML Thu Jan 25 11:59:52 2001 +0100
+++ b/doc-src/TutorialI/Misc/ROOT.ML Thu Jan 25 15:31:31 2001 +0100
@@ -11,3 +11,4 @@
use_thy "simp";
use_thy "Itrev";
use_thy "AdvancedInd";
+use_thy "appendix";
--- a/doc-src/TutorialI/Misc/document/natsum.tex Thu Jan 25 11:59:52 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Thu Jan 25 15:31:31 2001 +0100
@@ -43,8 +43,8 @@
\ttindexboldpos{\mystar}{$HOL2arithfun}, \isaindexbold{min},
\isaindexbold{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and
\ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available
- not just for natural numbers but at other types as well (see
- \S\ref{sec:overloading}). For example, given the goal \isa{x\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ x},
+ not just for natural numbers but at other types as well.
+ For example, given the goal \isa{x\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ x},
there is nothing to indicate that you are talking about natural numbers.
Hence Isabelle can only infer that \isa{x} is of some arbitrary type where
\isa{{\isadigit{0}}} and \isa{{\isacharplus}} are declared. As a consequence, you will be unable
@@ -54,6 +54,10 @@
\isa{x{\isacharplus}{\isadigit{0}}\ {\isacharequal}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}}. If there is enough contextual information this
may not be necessary: \isa{Suc\ x\ {\isacharequal}\ x} automatically implies
\isa{x{\isacharcolon}{\isacharcolon}nat} because \isa{Suc} is not overloaded.
+
+ For details see \S\ref{sec:numbers} and \S\ref{sec:overloading};
+ Table~\ref{tab:overloading} in the appendix shows the most important overloaded
+ operations.
\end{warn}
Simple arithmetic goals are proved automatically by both \isa{auto} and the
--- a/doc-src/TutorialI/Misc/natsum.thy Thu Jan 25 11:59:52 2001 +0100
+++ b/doc-src/TutorialI/Misc/natsum.thy Thu Jan 25 15:31:31 2001 +0100
@@ -41,8 +41,8 @@
\ttindexboldpos{\mystar}{$HOL2arithfun}, \isaindexbold{min},
\isaindexbold{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and
\ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available
- not just for natural numbers but at other types as well (see
- \S\ref{sec:overloading}). For example, given the goal @{prop"x+0 = x"},
+ not just for natural numbers but at other types as well.
+ For example, given the goal @{prop"x+0 = x"},
there is nothing to indicate that you are talking about natural numbers.
Hence Isabelle can only infer that @{term x} is of some arbitrary type where
@{term 0} and @{text"+"} are declared. As a consequence, you will be unable
@@ -52,6 +52,10 @@
@{text"x+0 = (x::nat)"}. If there is enough contextual information this
may not be necessary: @{prop"Suc x = x"} automatically implies
@{text"x::nat"} because @{term Suc} is not overloaded.
+
+ For details see \S\ref{sec:numbers} and \S\ref{sec:overloading};
+ Table~\ref{tab:overloading} in the appendix shows the most important overloaded
+ operations.
\end{warn}
Simple arithmetic goals are proved automatically by both @{term auto} and the
--- a/doc-src/TutorialI/Rules/rules.tex Thu Jan 25 11:59:52 2001 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex Thu Jan 25 15:31:31 2001 +0100
@@ -234,8 +234,8 @@
Recall that the conjunction elimination rules --- whose Isabelle names are
\isa{conjunct1} and \isa{conjunct2} --- simply return the first or second half
of a conjunction. Rules of this sort (where the conclusion is a subformula of a
-premise) are called \textbf{destruction} rules, by analogy with the destructor
-functions of functional programming.%
+premise) are called \textbf{destruction} rules because they take apart and destroy
+a premise.%
\footnote{This Isabelle terminology has no counterpart in standard logic texts,
although the distinction between the two forms of elimination rule is well known.
Girard \cite[page 74]{girard89}, for example, writes ``The elimination rules
@@ -365,7 +365,7 @@
conclusion.
\medskip
-\indexbold{by}
+\indexbold{*by}
The \isacommand{by} command is useful for proofs like these that use
\isa{assumption} heavily. It executes an
\isacommand{apply} command, then tries to prove all remaining subgoals using
@@ -781,7 +781,7 @@
To see how this works, let us derive a rule about reducing
the scope of a universal quantifier. In mathematical notation we write
\[ \infer{P\imp\forall x.\,Q}{\forall x.\,P\imp Q} \]
-with the proviso `$x$ not free in~$P$.' Isabelle's treatment of
+with the proviso ``$x$ not free in~$P$.'' Isabelle's treatment of
substitution makes the proviso unnecessary. The conclusion is expressed as
\isa{P\
\isasymlongrightarrow\ ({\isasymforall}x.\ Q\ x)}. No substitution for the
@@ -860,7 +860,7 @@
\isacommand{apply}\ (rename_tac\ v\ w)\isanewline
\ 1.\ \isasymAnd v\ w.\ x\ <\ y\ \isasymLongrightarrow \ P\ v\ (f\ w)
\end{isabelle}
-Recall that \isa{rule_tac}\index{rule_tac|and renaming} instantiates a
+Recall that \isa{rule_tac}\index{*rule_tac!and renaming} instantiates a
theorem with specified terms. These terms may involve the goal's bound
variables, but beware of referring to variables
like~\isa{xa}. A future change to your theories could change the set of names
@@ -1686,7 +1686,7 @@
The next step is to put
the theorem \isa{gcd_mult_0} into a simplified form, performing the steps
-$\gcd(1,n)=1$ and $k\times1=k$. The \isa{simplified}\indexbold{simplified}
+$\gcd(1,n)=1$ and $k\times1=k$. The \isaindexbold{simplified}
attribute takes a theorem
and returns the result of simplifying it, with respect to the default
simplification rules:
@@ -1769,7 +1769,7 @@
\end{isabelle}
\medskip
-The \isa{rule_format}\indexbold{rule_format} directive replaces a common usage
+The \isaindexbold{rule_format} directive replaces a common usage
of \isa{THEN}\@. It is needed in proofs by induction when the induction formula must be
expressed using
\isa{\isasymlongrightarrow} and \isa{\isasymforall}. For example, in
--- a/doc-src/TutorialI/Sets/sets.tex Thu Jan 25 11:59:52 2001 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex Thu Jan 25 15:31:31 2001 +0100
@@ -871,7 +871,7 @@
Many familiar induction principles are instances of this rule.
For example, the predecessor relation on the natural numbers
is well-founded; induction over it is mathematical induction.
-The `tail of' relation on lists is well-founded; induction over
+The ``tail of'' relation on lists is well-founded; induction over
it is structural induction.
Well-foundedness can be difficult to show. The various
--- a/doc-src/TutorialI/ToyList/ToyList.thy Thu Jan 25 11:59:52 2001 +0100
+++ b/doc-src/TutorialI/ToyList/ToyList.thy Thu Jan 25 15:31:31 2001 +0100
@@ -177,7 +177,7 @@
txt{*\noindent\index{*induct_tac}%
This tells Isabelle to perform induction on variable @{term"xs"}. The suffix
-@{term"tac"} stands for ``tactic'', a synonym for ``theorem proving function''.
+@{term"tac"} stands for \bfindex{tactic}, a synonym for ``theorem proving function''.
By default, induction acts on the first subgoal. The new proof state contains
two subgoals, namely the base case (@{term[source]Nil}) and the induction step
(@{term[source]Cons}):
@@ -207,7 +207,7 @@
txt{*\noindent
This command tells Isabelle to apply a proof strategy called
@{text"auto"} to all subgoals. Essentially, @{text"auto"} tries to
-``simplify'' the subgoals. In our case, subgoal~1 is solved completely (thanks
+simplify the subgoals. In our case, subgoal~1 is solved completely (thanks
to the equation @{prop"rev [] = []"}) and disappears; the simplified version
of subgoal~2 becomes the new subgoal~1:
@{subgoals[display,indent=0,margin=70]}
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex Thu Jan 25 11:59:52 2001 +0100
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Thu Jan 25 15:31:31 2001 +0100
@@ -172,7 +172,7 @@
\begin{isamarkuptxt}%
\noindent\index{*induct_tac}%
This tells Isabelle to perform induction on variable \isa{xs}. The suffix
-\isa{tac} stands for ``tactic'', a synonym for ``theorem proving function''.
+\isa{tac} stands for \bfindex{tactic}, a synonym for ``theorem proving function''.
By default, induction acts on the first subgoal. The new proof state contains
two subgoals, namely the base case (\isa{Nil}) and the induction step
(\isa{Cons}):
@@ -204,7 +204,7 @@
\noindent
This command tells Isabelle to apply a proof strategy called
\isa{auto} to all subgoals. Essentially, \isa{auto} tries to
-``simplify'' the subgoals. In our case, subgoal~1 is solved completely (thanks
+simplify the subgoals. In our case, subgoal~1 is solved completely (thanks
to the equation \isa{rev\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}) and disappears; the simplified version
of subgoal~2 becomes the new subgoal~1:
\begin{isabelle}%
--- a/doc-src/TutorialI/Trie/Trie.thy Thu Jan 25 11:59:52 2001 +0100
+++ b/doc-src/TutorialI/Trie/Trie.thy Thu Jan 25 15:31:31 2001 +0100
@@ -132,7 +132,7 @@
proof states are invisible, and we rely on the (possibly brittle) magic of
@{text auto} (@{text simp_all} will not do --- try it) to split the subgoals
of the induction up in such a way that case distinction on @{term bs} makes
-sense and solves the proof. Part~\ref{Isar} shows you how to write readable
+sense and solves the proof. Chapter~\ref{ch:Isar} shows you how to write readable
and stable proofs.
*};
--- a/doc-src/TutorialI/Trie/document/Trie.tex Thu Jan 25 11:59:52 2001 +0100
+++ b/doc-src/TutorialI/Trie/document/Trie.tex Thu Jan 25 15:31:31 2001 +0100
@@ -122,7 +122,7 @@
proof states are invisible, and we rely on the (possibly brittle) magic of
\isa{auto} (\isa{simp{\isacharunderscore}all} will not do --- try it) to split the subgoals
of the induction up in such a way that case distinction on \isa{bs} makes
-sense and solves the proof. Part~\ref{Isar} shows you how to write readable
+sense and solves the proof. Chapter~\ref{ch:Isar} shows you how to write readable
and stable proofs.%
\end{isamarkuptext}%
\end{isabellebody}%
--- a/doc-src/TutorialI/Types/Overloading2.thy Thu Jan 25 11:59:52 2001 +0100
+++ b/doc-src/TutorialI/Types/Overloading2.thy Thu Jan 25 15:31:31 2001 +0100
@@ -22,38 +22,10 @@
text{*
HOL comes with a number of overloaded constants and corresponding classes.
-The most important ones are listed in Table~\ref{tab:overloading}. They are
+The most important ones are listed in Table~\ref{tab:overloading} in the appendix. They are
defined on all numeric types and sometimes on other types as well, for example
@{text"-"}, @{text"\<le>"} and @{text"<"} on sets.
-\begin{table}[htbp]
-\begin{center}
-\begin{tabular}{lll}
-Constant & Type & Syntax \\
-\hline
-@{term 0} & @{text "'a::zero"} \\
-@{text"+"} & @{text "('a::plus) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 65) \\
-@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 65) \\
-@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a"} \\
-@{text"*"} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
-@{text div} & @{text "('a::div) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
-@{text mod} & @{text "('a::div) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
-@{text dvd} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
-@{text"/"} & @{text "('a::inverse) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
-@{text"^"} & @{text "('a::power) \<Rightarrow> nat \<Rightarrow> 'a"} & (infixr 80) \\
-@{term abs} & @{text "('a::minus) \<Rightarrow> 'a"} & ${\mid} x {\mid}$\\
-@{text"\<le>"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
-@{text"<"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
-@{term min} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\
-@{term max} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\
-@{term Least} & @{text "('a::ord \<Rightarrow> bool) \<Rightarrow> 'a"} &
-@{text LEAST}$~x.~P$
-\end{tabular}
-\caption{Overloaded Constants in HOL}
-\label{tab:overloading}
-\end{center}
-\end{table}
-
In addition there is a special input syntax for bounded quantifiers:
\begin{center}
\begin{tabular}{lcl}
--- a/doc-src/TutorialI/Types/document/Overloading2.tex Thu Jan 25 11:59:52 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading2.tex Thu Jan 25 15:31:31 2001 +0100
@@ -24,38 +24,10 @@
%
\begin{isamarkuptext}%
HOL comes with a number of overloaded constants and corresponding classes.
-The most important ones are listed in Table~\ref{tab:overloading}. They are
+The most important ones are listed in Table~\ref{tab:overloading} in the appendix. They are
defined on all numeric types and sometimes on other types as well, for example
\isa{{\isacharminus}}, \isa{{\isasymle}} and \isa{{\isacharless}} on sets.
-\begin{table}[htbp]
-\begin{center}
-\begin{tabular}{lll}
-Constant & Type & Syntax \\
-\hline
-\isa{{\isadigit{0}}} & \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}zero} \\
-\isa{{\isacharplus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}plus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 65) \\
-\isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 65) \\
-\isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} \\
-\isa{{\isacharasterisk}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}times{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
-\isa{div} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}div{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
-\isa{mod} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}div{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
-\isa{dvd} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}times{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
-\isa{{\isacharslash}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}inverse{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
-\isa{{\isacharcircum}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}power{\isacharparenright}\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a} & (infixr 80) \\
-\isa{abs} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} & ${\mid} x {\mid}$\\
-\isa{{\isasymle}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
-\isa{{\isacharless}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
-\isa{min} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\
-\isa{max} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\
-\isa{Least} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} &
-\isa{LEAST}$~x.~P$
-\end{tabular}
-\caption{Overloaded Constants in HOL}
-\label{tab:overloading}
-\end{center}
-\end{table}
-
In addition there is a special input syntax for bounded quantifiers:
\begin{center}
\begin{tabular}{lcl}
--- a/doc-src/TutorialI/Types/numerics.tex Thu Jan 25 11:59:52 2001 +0100
+++ b/doc-src/TutorialI/Types/numerics.tex Thu Jan 25 15:31:31 2001 +0100
@@ -6,7 +6,10 @@
\isa{int} of \textbf{integers}, which lack induction but support true
subtraction. The logic HOL-Real also has the type \isa{real} of real
numbers. Isabelle has no subtyping, so the numeric types are distinct and
-there are functions to convert between them.
+there are functions to convert between them. Fortunately most numeric
+operations are overloaded: the same symbol can be used at all numeric types.
+Table~\ref{tab:overloading} in the appendix shows the most important operations,
+together with the priorities of the infix symbols.
The integers are preferable to the natural numbers for reasoning about
complicated arithmetic expressions. For example, a termination proof
--- a/doc-src/TutorialI/appendix.tex Thu Jan 25 11:59:52 2001 +0100
+++ b/doc-src/TutorialI/appendix.tex Thu Jan 25 15:31:31 2001 +0100
@@ -3,7 +3,7 @@
\chapter{Appendix}
\label{sec:Appendix}
-\begin{figure}[htbp]
+\begin{table}[htbp]
\begin{center}
\begin{tabular}{|l|l|l|}
\hline
@@ -98,11 +98,13 @@
\hline
\end{tabular}
\end{center}
-\caption{Mathematical symbols, their ASCII-equivalents and ProofGeneral codes}
-\label{fig:ascii}
-\end{figure}\indexbold{ASCII symbols}
+\caption{Mathematical symbols, their ASCII-equivalents and X-Symbol codes}
+\label{tab:ascii}
+\end{table}\indexbold{ASCII symbols}
-\begin{figure}[htbp]
+\input{Misc/document/appendix.tex}
+
+\begin{table}[htbp]
\begin{center}
\begin{tabular}{|lllllllll|}
\hline
@@ -143,11 +145,11 @@
\end{tabular}
\end{center}
\caption{Reserved words in HOL terms}
-\label{fig:ReservedWords}
-\end{figure}
+\label{tab:ReservedWords}
+\end{table}
-%\begin{figure}[htbp]
+%\begin{table}[htbp]
%\begin{center}
%\begin{tabular}{|lllll|}
%\hline
@@ -175,5 +177,5 @@
%\end{tabular}
%\end{center}
%\caption{Minor keywords in HOL theories}
-%\label{fig:keywords}
-%\end{figure}
+%\label{tab:keywords}
+%\end{table}
--- a/doc-src/TutorialI/basics.tex Thu Jan 25 11:59:52 2001 +0100
+++ b/doc-src/TutorialI/basics.tex Thu Jan 25 15:31:31 2001 +0100
@@ -62,7 +62,7 @@
HOL's theory collection is available online at
\begin{center}\small
- \url{http://isabelle.in.tum.de/library/}
+ \url{http://isabelle.in.tum.de/library/HOL/}
\end{center}
and is recommended browsing. Note that most of the theories
are based on classical Isabelle without the Isar extension. This means that
@@ -233,7 +233,7 @@
\end{itemize}
For the sake of readability the usual mathematical symbols are used throughout
-the tutorial. Their ASCII-equivalents are shown in figure~\ref{fig:ascii} in
+the tutorial. Their ASCII-equivalents are shown in table~\ref{tab:ascii} in
the appendix.
@@ -279,7 +279,7 @@
Some interfaces (including the shell level) offer special fonts with
mathematical symbols. For those that do not, remember that ASCII-equivalents
-are shown in figure~\ref{fig:ascii} in the appendix.
+are shown in table~\ref{tab:ascii} in the appendix.
Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}}
Commands may but need not be terminated by semicolons.
--- a/doc-src/TutorialI/fp.tex Thu Jan 25 11:59:52 2001 +0100
+++ b/doc-src/TutorialI/fp.tex Thu Jan 25 15:31:31 2001 +0100
@@ -129,10 +129,10 @@
\isa{\isacommand{theory}~T~=~\dots~:} is processed, the
modified parent is reloaded automatically.
- The only time when you need to load a theory by hand is when you simply
- want to check if it loads successfully without wanting to make use of the
- theory itself. This you can do by typing
- \isa{\isacommand{use\_thy}\indexbold{*use_thy}~"T"}.
+% The only time when you need to load a theory by hand is when you simply
+% want to check if it loads successfully without wanting to make use of the
+% theory itself. This you can do by typing
+% \isa{\isacommand{use\_thy}\indexbold{*use_thy}~"T"}.
\end{description}
Further commands are found in the Isabelle/Isar Reference Manual.
@@ -302,7 +302,7 @@
section as well, in particular in order to understand what happened if things
do not simplify as expected.
-\subsubsection{What is Simplification?}
+\subsubsection{What is Simplification}
In its most basic form, simplification means repeated application of
equations from left to right. For example, taking the rules for \isa{\at}
--- a/doc-src/TutorialI/tutorial.tex Thu Jan 25 11:59:52 2001 +0100
+++ b/doc-src/TutorialI/tutorial.tex Thu Jan 25 15:31:31 2001 +0100
@@ -91,6 +91,7 @@
\chapter{Theory Presentation}
\chapter{Case Study: Verifying a Cryptographic Protocol}
\chapter{Structured Proofs}
+\label{ch:Isar}
%\chapter{Case Study: UNIX File-System Security}
%\chapter{The Tricks of the Trade}
\input{appendix}