# HG changeset patch
# User nipkow
# Date 1007037225 -3600
# Node ID 5a4d782044924026ad49cb05fe59461073b46935
# Parent  b4e706774e961defe02f691b8abe8b344c9d4a84
*** empty log message ***

diff -r b4e706774e96 -r 5a4d78204492 doc-src/TutorialI/Ifexpr/Ifexpr.thy
--- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Thu Nov 29 01:51:38 2001 +0100
+++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Thu Nov 29 13:33:45 2001 +0100
@@ -162,7 +162,7 @@
 normality of @{term"normif"}:
 *}
 
-lemma[simp]: "\<forall>t e. normal(normif b t e) = (normal t \<and> normal e)";
+lemma [simp]: "\<forall>t e. normal(normif b t e) = (normal t \<and> normal e)";
 (*<*)
 apply(induct_tac b);
 by(auto);
diff -r b4e706774e96 -r 5a4d78204492 doc-src/TutorialI/Ifexpr/document/Ifexpr.tex
--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Thu Nov 29 01:51:38 2001 +0100
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Thu Nov 29 13:33:45 2001 +0100
@@ -187,7 +187,7 @@
 normality of \isa{normif}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{lemma}{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ normal{\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ normal{\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
diff -r b4e706774e96 -r 5a4d78204492 doc-src/TutorialI/Misc/document/natsum.tex
--- a/doc-src/TutorialI/Misc/document/natsum.tex	Thu Nov 29 01:51:38 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/natsum.tex	Thu Nov 29 13:33:45 2001 +0100
@@ -39,37 +39,38 @@
 \sdx{div}, \sdx{mod}, \cdx{min} and
 \cdx{max} are predefined, as are the relations
 \indexboldpos{\isasymle}{$HOL2arithrel} and
-\ttindexboldpos{<}{$HOL2arithrel}. As usual, \isa{m\ {\isacharminus}\ n\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}} if
+\ttindexboldpos{<}{$HOL2arithrel}. As usual, \isa{m\ {\isacharminus}\ n\ {\isacharequal}\ {\isadigit{0}}} if
 \isa{m\ {\isacharless}\ n}. There is even a least number operation
-\sdx{LEAST}\@.  For example, \isa{{\isacharparenleft}LEAST\ n{\isachardot}\ {\isacharparenleft}{\isadigit{1}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharless}\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{2}}{\isasymColon}{\isacharprime}a{\isacharparenright}}. 
-\REMARK{Isabelle CAN prove it automatically, using \isa{auto intro: Least_equality}.
- The following needs changing with our new system of numbers.}
-Note that \isa{{\isadigit{1}}{\isasymColon}{\isacharprime}a}
-and \isa{{\isadigit{2}}{\isasymColon}{\isacharprime}a} are available as abbreviations for the corresponding
-\isa{Suc}-expressions. If you need the full set of numerals,
-see~\S\ref{sec:numerals}.
-
+\sdx{LEAST}\@.  For example, \isa{{\isacharparenleft}LEAST\ n{\isachardot}\ {\isadigit{0}}\ {\isacharless}\ n{\isacharparenright}\ {\isacharequal}\ Suc\ {\isadigit{0}}}.
 \begin{warn}\index{overloading}
-  The constant \cdx{0} and the operations
+  The constants \cdx{0} and \cdx{1} and the operations
   \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
   \ttindexboldpos{\mystar}{$HOL2arithfun}, \cdx{min},
   \cdx{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.
-  For example, given the goal \isa{x\ {\isacharplus}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\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}}{\isasymColon}{\isacharprime}a} and \isa{{\isacharplus}} are declared. As a consequence, you will be unable
-  to prove the goal (although it may take you some time to realize what has
-  happened if \isa{show{\isacharunderscore}types} is not set).  In this particular example,
-  you need to include an explicit type constraint, for example
-  \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 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 to prove the
+  goal. To alert you to such pitfalls, Isabelle flags numerals without a
+  fixed type in its output: \isa{x\ {\isacharplus}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharequal}\ x}. (In the absence of a numeral,
+  it may take you some time to realize what has happened if \isa{show{\isacharunderscore}types} is not set).  In this particular example, you need to include
+  an explicit type constraint, for example \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.
+  For details on overloading see \S\ref{sec:overloading}.
+  Table~\ref{tab:overloading} in the appendix shows the most important
+  overloaded operations.
+\end{warn}
+\begin{warn}
+  Constant \isa{{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat} is defined to be \isa{Suc\ {\isadigit{0}}}. This definition
+  (see \S\ref{sec:ConstDefinitions}) is unfolded automatically by some
+  tactics (like \isa{auto}, \isa{simp} and \isa{arith}) but not by
+  others (especially the single step tactics in Chapter~\ref{chap:rules}).
+  If you need the full set of numerals, see~\S\ref{sec:numerals}.
+  \emph{Novices are advised to stick to \isa{{\isadigit{0}}} and of \isa{Suc}.}
 \end{warn}
 
 Both \isa{auto} and \isa{simp}
diff -r b4e706774e96 -r 5a4d78204492 doc-src/TutorialI/Misc/natsum.thy
--- a/doc-src/TutorialI/Misc/natsum.thy	Thu Nov 29 01:51:38 2001 +0100
+++ b/doc-src/TutorialI/Misc/natsum.thy	Thu Nov 29 13:33:45 2001 +0100
@@ -28,37 +28,40 @@
 \sdx{div}, \sdx{mod}, \cdx{min} and
 \cdx{max} are predefined, as are the relations
 \indexboldpos{\isasymle}{$HOL2arithrel} and
-\ttindexboldpos{<}{$HOL2arithrel}. As usual, @{prop"m-n = 0"} if
+\ttindexboldpos{<}{$HOL2arithrel}. As usual, @{prop"m-n = (0::nat)"} if
 @{prop"m<n"}. There is even a least number operation
-\sdx{LEAST}\@.  For example, @{prop"(LEAST n. 1 < n) = 2"}. 
-\REMARK{Isabelle CAN prove it automatically, using \isa{auto intro: Least_equality}.
- The following needs changing with our new system of numbers.}
-Note that @{term 1}
-and @{term 2} are available as abbreviations for the corresponding
-@{term Suc}-expressions. If you need the full set of numerals,
-see~\S\ref{sec:numerals}.
-
+\sdx{LEAST}\@.  For example, @{prop"(LEAST n. 0 < n) = Suc 0"}.
 \begin{warn}\index{overloading}
-  The constant \cdx{0} and the operations
+  The constants \cdx{0} and \cdx{1} and the operations
   \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
   \ttindexboldpos{\mystar}{$HOL2arithfun}, \cdx{min},
   \cdx{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.
-  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
-  to prove the goal (although it may take you some time to realize what has
-  happened if @{text show_types} is not set).  In this particular example,
-  you need to include an explicit type constraint, for example
-  @{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 example, given the goal @{text"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 @{text 0} and @{text"+"} are
+  declared. As a consequence, you will be unable to prove the
+  goal. To alert you to such pitfalls, Isabelle flags numerals without a
+  fixed type in its output: @{prop"x+0 = x"}. (In the absence of a numeral,
+  it may take you some time to realize what has happened if @{text
+  show_types} is not set).  In this particular example, you need to include
+  an explicit type constraint, for example @{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.
+  For details on overloading see \S\ref{sec:overloading}.
+  Table~\ref{tab:overloading} in the appendix shows the most important
+  overloaded operations.
+\end{warn}
+\begin{warn}
+  Constant @{text"1::nat"} is defined to be @{term"Suc 0"}. This definition
+  (see \S\ref{sec:ConstDefinitions}) is unfolded automatically by some
+  tactics (like @{text auto}, @{text simp} and @{text arith}) but not by
+  others (especially the single step tactics in Chapter~\ref{chap:rules}).
+  If you need the full set of numerals, see~\S\ref{sec:numerals}.
+  \emph{Novices are advised to stick to @{term"0::nat"} and @{term Suc}.}
 \end{warn}
 
 Both @{text auto} and @{text simp}
diff -r b4e706774e96 -r 5a4d78204492 doc-src/TutorialI/Misc/types.thy
--- a/doc-src/TutorialI/Misc/types.thy	Thu Nov 29 01:51:38 2001 +0100
+++ b/doc-src/TutorialI/Misc/types.thy	Thu Nov 29 13:33:45 2001 +0100
@@ -1,7 +1,7 @@
 (*<*)theory "types" = Main:(*>*)
 types number       = nat
       gate         = "bool \<Rightarrow> bool \<Rightarrow> bool"
-      ('a,'b)alist = "('a \<times> 'b)list";
+      ('a,'b)alist = "('a \<times> 'b)list"
 
 text{*\noindent
 Internally all synonyms are fully expanded.  As a consequence Isabelle's
@@ -11,7 +11,7 @@
 *}
 
 consts nand :: gate
-       xor  :: gate;
+       xor  :: gate
 
 subsection{*Constant Definitions*}
 
@@ -21,7 +21,7 @@
 *}
 
 defs nand_def: "nand A B \<equiv> \<not>(A \<and> B)"
-     xor_def:  "xor A B  \<equiv> A \<and> \<not>B \<or> \<not>A \<and> B";
+     xor_def:  "xor A B  \<equiv> A \<and> \<not>B \<or> \<not>A \<and> B"
 
 text{*\noindent%
 Here \commdx{defs} is a keyword and
@@ -41,7 +41,7 @@
 constdefs nor :: gate
          "nor A B \<equiv> \<not>(A \<or> B)"
           xor2 :: gate
-         "xor2 A B \<equiv> (A \<or> B) \<and> (\<not>A \<or> \<not>B)";
+         "xor2 A B \<equiv> (A \<or> B) \<and> (\<not>A \<or> \<not>B)"
 
 text{*\noindent
 The default name of each definition is $f$@{text"_def"}, where
diff -r b4e706774e96 -r 5a4d78204492 doc-src/TutorialI/ToyList/ToyList.thy
--- a/doc-src/TutorialI/ToyList/ToyList.thy	Thu Nov 29 01:51:38 2001 +0100
+++ b/doc-src/TutorialI/ToyList/ToyList.thy	Thu Nov 29 13:33:45 2001 +0100
@@ -13,8 +13,8 @@
                  | Cons 'a "'a list"            (infixr "#" 65);
 
 text{*\noindent
-\index{datatype@\isacommand {datatype} (command)}
-The datatype \tydx{list} introduces two
+The datatype\index{datatype@\isacommand {datatype} (command)}
+\tydx{list} introduces two
 constructors \cdx{Nil} and \cdx{Cons}, the
 empty~list and the operator that adds an element to the front of a list. For
 example, the term \isa{Cons True (Cons False Nil)} is a value of
@@ -142,7 +142,7 @@
 @{term"xs"}.
 \end{itemize}
 The name and the simplification attribute are optional.
-Isabelle's response is to print
+Isabelle's response is to print the initial proof state
 \begin{isabelle}
 proof(prove):~step~0\isanewline
 \isanewline
@@ -187,7 +187,7 @@
 
 The induction step is an example of the general format of a subgoal:\index{subgoals}
 \begin{isabelle}
-~$i$.~{\isasymAnd}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
+~$i$.~{\isasymAnd}$x\sb{1}$~\dots$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
 \end{isabelle}\index{$IsaAnd@\isasymAnd|bold}
 The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
 ignored most of the time, or simply treated as a list of variables local to
diff -r b4e706774e96 -r 5a4d78204492 doc-src/TutorialI/ToyList/document/ToyList.tex
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Thu Nov 29 01:51:38 2001 +0100
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Thu Nov 29 13:33:45 2001 +0100
@@ -18,8 +18,8 @@
 %
 \begin{isamarkuptext}%
 \noindent
-\index{datatype@\isacommand {datatype} (command)}
-The datatype \tydx{list} introduces two
+The datatype\index{datatype@\isacommand {datatype} (command)}
+\tydx{list} introduces two
 constructors \cdx{Nil} and \cdx{Cons}, the
 empty~list and the operator that adds an element to the front of a list. For
 example, the term \isa{Cons True (Cons False Nil)} is a value of
@@ -150,7 +150,7 @@
 \isa{xs}.
 \end{itemize}
 The name and the simplification attribute are optional.
-Isabelle's response is to print
+Isabelle's response is to print the initial proof state
 \begin{isabelle}
 proof(prove):~step~0\isanewline
 \isanewline
@@ -200,7 +200,7 @@
 
 The induction step is an example of the general format of a subgoal:\index{subgoals}
 \begin{isabelle}
-~$i$.~{\isasymAnd}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
+~$i$.~{\isasymAnd}$x\sb{1}$~\dots$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
 \end{isabelle}\index{$IsaAnd@\isasymAnd|bold}
 The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
 ignored most of the time, or simply treated as a list of variables local to
diff -r b4e706774e96 -r 5a4d78204492 doc-src/TutorialI/basics.tex
--- a/doc-src/TutorialI/basics.tex	Thu Nov 29 01:51:38 2001 +0100
+++ b/doc-src/TutorialI/basics.tex	Thu Nov 29 13:33:45 2001 +0100
@@ -35,7 +35,8 @@
 introduces the rudiments of Isar's proof language. To fully exploit the power
 of Isar, in particular the ability to write readable and structured proofs,
 you need to consult the Isabelle/Isar Reference
-Manual~\cite{isabelle-isar-ref}. If you want to use Isabelle's ML level
+Manual~\cite{isabelle-isar-ref} and Wenzel's PhD thesis~\cite{Wenzel-PhD}
+which discusses many proof patterns. If you want to use Isabelle's ML level
 directly (for example for writing your own proof procedures) see the Isabelle
 Reference Manual~\cite{isabelle-ref}; for details relating to HOL see the
 Isabelle/HOL manual~\cite{isabelle-HOL}. All manuals have a comprehensive
@@ -70,7 +71,8 @@
 This tutorial is concerned with introducing you to the different linguistic
 constructs that can fill the \textit{declarations, definitions, and
     proofs} above.  A complete grammar of the basic
-constructs is found in the Isabelle/Isar Reference Manual.
+constructs is found in the Isabelle/Isar Reference
+Manual~\cite{isabelle-isar-ref}.
 
 HOL's theory collection is available online at
 \begin{center}\small
@@ -244,11 +246,10 @@
 \isa{\isasymlambda}, and quantifiers.
 \item
 Never write \isa{\isasymlambda{}x.x} or \isa{\isasymforall{}x.x=x}
-because \isa{x.x} is always taken as a single qualified identifier that
-refers to an item \isa{x} in theory \isa{x}. Write
+because \isa{x.x} is always taken as a single qualified identifier. Write
 \isa{\isasymlambda{}x.~x} and \isa{\isasymforall{}x.~x=x} instead.
 \item Identifiers\indexbold{identifiers} may contain the characters \isa{_} 
-and~\isa{'}.
+and~\isa{'}, except at the beginning.
 \end{itemize}
 
 For the sake of readability, we use the usual mathematical symbols throughout
diff -r b4e706774e96 -r 5a4d78204492 doc-src/TutorialI/fp.tex
--- a/doc-src/TutorialI/fp.tex	Thu Nov 29 01:51:38 2001 +0100
+++ b/doc-src/TutorialI/fp.tex	Thu Nov 29 13:33:45 2001 +0100
@@ -37,8 +37,9 @@
 The complete proof script is shown in Fig.\ts\ref{fig:ToyList-proofs}. The
 concatenation of Figs.\ts\ref{fig:ToyList} and~\ref{fig:ToyList-proofs}
 constitutes the complete theory \texttt{ToyList} and should reside in file
-\texttt{ToyList.thy}. It is good practice to present all declarations and
-definitions at the beginning of a theory to facilitate browsing.%
+\texttt{ToyList.thy}.
+% It is good practice to present all declarations and
+%definitions at the beginning of a theory to facilitate browsing.%
 \index{*ToyList example|)}
 
 \begin{figure}[htbp]
@@ -70,7 +71,7 @@
 There are two kinds of commands used during a proof: the actual proof
 commands and auxiliary commands for examining the proof state and controlling
 the display. Simple proof commands are of the form
-\commdx{apply}\isa{(\textit{method})}, where \textit{method} is typically 
+\commdx{apply}(\textit{method}), where \textit{method} is typically 
 \isa{induct_tac} or \isa{auto}.  All such theorem proving operations
 are referred to as \bfindex{methods}, and further ones are
 introduced throughout the tutorial.  Unless stated otherwise, you may
@@ -144,7 +145,8 @@
 %  theory itself. This you can do by typing
 %  \isa{\commdx{use\_thy}~"T"}.
 \end{description}
-Further commands are found in the Isabelle/Isar Reference Manual.
+Further commands are found in the Isabelle/Isar Reference
+Manual~\cite{isabelle-isar-ref}.
 
 We now examine Isabelle's functional programming constructs systematically,
 starting with inductive datatypes.
@@ -175,7 +177,7 @@
 Theory \isa{List} also contains
 more syntactic sugar: \isa{[}$x@1$\isa{,}\dots\isa{,}$x@n$\isa{]} abbreviates
 $x@1$\isa{\#}\dots\isa{\#}$x@n$\isa{\#[]}.  In the rest of the tutorial we
-always use HOL's predefined lists.
+always use HOL's predefined lists by building on theory \isa{Main}.
 
 
 \subsection{The General Format}
@@ -198,10 +200,12 @@
 during proofs by simplification.  The same is true for the equations in
 primitive recursive function definitions.
 
-Every datatype $t$ comes equipped with a \isa{size} function from $t$ into
-the natural numbers (see~{\S}\ref{sec:nat} below). For lists, \isa{size} is
-just the length, i.e.\ \isa{size [] = 0} and \isa{size(x \# xs) = size xs +
-  1}.  In general, \cdx{size} returns 
+Every\footnote{Except for advanced datatypes where the recursion involves
+``\isasymRightarrow'' as in {\S}\ref{sec:nested-fun-datatype}.} datatype $t$
+comes equipped with a \isa{size} function from $t$ into the natural numbers
+(see~{\S}\ref{sec:nat} below). For lists, \isa{size} is just the length, i.e.\
+\isa{size [] = 0} and \isa{size(x \# xs) = size xs + 1}.  In general,
+\cdx{size} returns
 \begin{itemize}
 \item zero for all constructors
 that do not have an argument of type $t$\\
@@ -275,12 +279,11 @@
 
 \subsection{Type Synonyms}
 
-\index{type synonyms|(}%
+\index{type synonyms}%
 Type synonyms are similar to those found in ML\@. They are created by a 
 \commdx{types} command:
 
-\input{Misc/document/types.tex}%
-\index{type synonyms|)}
+\input{Misc/document/types.tex}
 
 \input{Misc/document/prime_def.tex}
 
@@ -397,6 +400,7 @@
 
 
 \subsection{The Limits of Nested Recursion}
+\label{sec:nested-fun-datatype}
 
 How far can we push nested recursion? By the unfolding argument above, we can
 reduce nested to mutual recursion provided the nested recursion only involves
diff -r b4e706774e96 -r 5a4d78204492 doc-src/TutorialI/preface.tex
--- a/doc-src/TutorialI/preface.tex	Thu Nov 29 01:51:38 2001 +0100
+++ b/doc-src/TutorialI/preface.tex	Thu Nov 29 13:33:45 2001 +0100
@@ -16,9 +16,11 @@
 eight simplification tactics with a single method, namely \isa{simp},
 with associated options.
 
-The typesetting relies on Wenzel's proof presentation tools.  A possibly
-annotated theory file is run, typesetting the theory and any requested
-Isabelle responses in the form of a \TeX{} source file.  This book is
+\REMARK{mention Wenzel once author?}
+The typesetting relies on Wenzel's theory presentation tools.  An
+annotated source file is run, typesetting the theory
+% and any requested Isabelle responses
+in the form of a \TeX\ source file.  This book is
 derived almost entirely from output generated in this way.
 
 This tutorial owes a lot to the constant discussions with and the valuable