--- a/doc-src/TutorialI/Inductive/advanced-examples.tex Thu Nov 29 21:12:37 2001 +0100
+++ b/doc-src/TutorialI/Inductive/advanced-examples.tex Fri Nov 30 12:18:14 2001 +0100
@@ -144,8 +144,10 @@
\isakeyword{monos}\ lists_mono
\end{isabelle}
-We must cite the theorem \isa{lists_mono} in order to justify
-using the function \isa{lists}.
+We cite the theorem \isa{lists_mono} to justify
+using the function \isa{lists}.%
+\footnote{This particular theorem is installed by default already, but we
+include the \isakeyword{monos} declaration in order to illustrate its syntax.}
\begin{isabelle}
A\ \isasymsubseteq\ B\ \isasymLongrightarrow \ lists\ A\ \isasymsubseteq
\ lists\ B\rulenamedx{lists_mono}
--- a/doc-src/TutorialI/Misc/document/simp.tex Thu Nov 29 21:12:37 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex Fri Nov 30 12:18:14 2001 +0100
@@ -48,7 +48,7 @@
\end{warn}
\begin{warn}
It is inadvisable to toggle the simplification attribute of a
- theorem from a \emph{parent} theory $A$ in a child theory $B$ for good.
+ theorem from a parent theory $A$ in a child theory $B$ for good.
The reason is that if some theory $C$ is based both on $B$ and (via a
differnt path) on $A$, it is not defined what the simplification attribute
of that theorem will be in $C$: it could be either.
--- a/doc-src/TutorialI/Rules/rules.tex Thu Nov 29 21:12:37 2001 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex Fri Nov 30 12:18:14 2001 +0100
@@ -81,7 +81,11 @@
it yields new subgoals given by the formulas assigned to
\isa{?P} and \isa{?Q}.
-The following trivial proof illustrates this point.
+The following trivial proof illustrates how rules work. It also introduces a
+style of indentation. If a command adds a new subgoal, then the next
+command's indentation is increased by one space; if it proves a subgoal, then
+the indentation is reduced. This provides the reader with hints about the
+subgoal structure.
\begin{isabelle}
\isacommand{lemma}\ conj_rule:\ "\isasymlbrakk P;\
Q\isasymrbrakk\ \isasymLongrightarrow\ P\ \isasymand\
@@ -1806,8 +1810,8 @@
\ \ \ \ "gcd\ (m,n)\ =\ (if\ n=0\ then\ m\ else\ gcd(n,\ m\ mod\ n))"
\end{isabelle}
%
-From this definition, it is possible to prove the
-distributive law.
+From this definition, it is possible to prove the distributive law.
+That takes us to the starting point for our example.
\begin{isabelle}
?k\ *\ gcd\ (?m,\ ?n)\ =\ gcd\ (?k\ *\ ?m,\ ?k\ *\ ?n)
\rulename{gcd_mult_distrib2}
@@ -1947,7 +1951,8 @@
\rulename{dvd_def}
\end{isabelle}
%
-For example, this rule states that if $k$ and $n$ are relatively prime
+Suppose, for example, that we have proved the following rule.
+It states that if $k$ and $n$ are relatively prime
and if $k$ divides $m\times n$ then $k$ divides $m$.
\begin{isabelle}
\isasymlbrakk gcd(?k,?n){=}1;\ ?k\ dvd\ ?m * ?n\isasymrbrakk\
--- a/doc-src/TutorialI/Types/numerics.tex Thu Nov 29 21:12:37 2001 +0100
+++ b/doc-src/TutorialI/Types/numerics.tex Fri Nov 30 12:18:14 2001 +0100
@@ -424,7 +424,8 @@
defined for the reals, along with many theorems such as this one about
exponentiation:
\begin{isabelle}
-\isasymbar r\isasymbar \ \isacharcircum \ n\ =\ \isasymbar r\ \isacharcircum \ n\isasymbar
+\isasymbar r\ \isacharcircum \ n\isasymbar\ =\
+\isasymbar r\isasymbar \ \isacharcircum \ n
\rulename{realpow_abs}
\end{isabelle}
@@ -462,5 +463,8 @@
about limits, differentiation and integration~\cite{fleuriot-jcm}. The
development defines an infinitely large number, \isa{omega} and an
infinitely small positive number, \isa{epsilon}. The
-relation $x\approx y$ means ``$x$ is infinitely close to~$y$''.%
+relation $x\approx y$ means ``$x$ is infinitely close to~$y$.''
+Theory \isa{Hyperreal} also defines transcendental functions such as sine,
+cosine, exponential and logarithm --- even the versions for type
+\isa{real}, because they are defined using nonstandard limits.%
\index{numbers|)}
\ No newline at end of file
--- a/doc-src/TutorialI/tutorial.ind Thu Nov 29 21:12:37 2001 +0100
+++ b/doc-src/TutorialI/tutorial.ind Fri Nov 30 12:18:14 2001 +0100
@@ -38,7 +38,7 @@
\indexspace
\item \isa {0} (constant), 22, 23, 140
- \item \isa {1} (constant), 140, 141
+ \item \isa {1} (constant), 23, 140, 141
\indexspace
@@ -336,7 +336,7 @@
\item lexicographic product, \bold{105}, 166
\item {\texttt{lfp}}
\subitem applications of, \see{CTL}{106}
- \item linear arithmetic, 22--23, 139
+ \item linear arithmetic, 22--24, 139
\item \isa {List} (theory), 17
\item \isa {list} (type), 4, 9, 17
\item \isa {list.split} (theorem), 32
@@ -347,12 +347,12 @@
\item \isa {Main} (theory), 4
\item major premise, \bold{65}
- \item \isa {max} (constant), 23
+ \item \isa {max} (constant), 23, 24
\item measure functions, 47, 104
\item \isa {measure_def} (theorem), \bold{105}
\item meta-logic, \bold{70}
\item methods, \bold{15}
- \item \isa {min} (constant), 23
+ \item \isa {min} (constant), 23, 24
\item \isa {mod} (symbol), 23
\item \isa {mod_div_equality} (theorem), \bold{141}
\item \isa {mod_mult_distrib} (theorem), \bold{141}