# HG changeset patch
# User paulson
# Date 1007119094 -3600
# Node ID ef43a3d6e962460e175ecd56b005de394df9dd87
# Parent  aea72a834c85bf6e0278840b72a937f7b051d149
minor tweaks

diff -r aea72a834c85 -r ef43a3d6e962 doc-src/TutorialI/Inductive/advanced-examples.tex
--- 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}
diff -r aea72a834c85 -r ef43a3d6e962 doc-src/TutorialI/Misc/document/simp.tex
--- 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.
diff -r aea72a834c85 -r ef43a3d6e962 doc-src/TutorialI/Rules/rules.tex
--- 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\
diff -r aea72a834c85 -r ef43a3d6e962 doc-src/TutorialI/Types/numerics.tex
--- 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
diff -r aea72a834c85 -r ef43a3d6e962 doc-src/TutorialI/tutorial.ind
--- 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}