
diff -r a39e5d43de55 -r bbefb6ce5cb2 doc-src/TutorialI/ToyList/document/ToyList.tex
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Fri Sep 01 18:29:52 2000 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Fri Sep 01 19:09:44 2000 +0200
@@ -17,23 +17,24 @@
 The datatype\index{*datatype} \isaindexbold{list} introduces two
 constructors \isaindexbold{Nil} and \isaindexbold{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 type
-\isa{bool\ list}, namely the list with the elements \isa{True} and
+example, the term \isa{Cons True (Cons False Nil)} is a value of
+type \isa{bool\ list}, namely the list with the elements \isa{True} and
 \isa{False}. Because this notation becomes unwieldy very quickly, the
 datatype declaration is annotated with an alternative syntax: instead of
 \isa{Nil} and \isa{Cons x xs} we can write
-\isa{[]}\index{$HOL2list@\texttt{[]}|bold} and
-\isa{\mbox{x}\ {\isacharhash}\ \mbox{xs}}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
+\isa{{\isacharbrackleft}{\isacharbrackright}}\index{$HOL2list@\texttt{[]}|bold} and
+\isa{x\ {\isacharhash}\ xs}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
 alternative syntax is the standard syntax. Thus the list \isa{Cons True
 (Cons False Nil)} becomes \isa{True\ {\isacharhash}\ False\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}}. The annotation
-\isacommand{infixr}\indexbold{*infixr} means that \isa{\#} associates to
-the right, i.e.\ the term \isa{\mbox{x}\ {\isacharhash}\ \mbox{y}\ {\isacharhash}\ \mbox{z}} is read as \isa{x
-\# (y \# z)} and not as \isa{(x \# y) \# z}.
+\isacommand{infixr}\indexbold{*infixr} means that \isa{{\isacharhash}} associates to
+the right, i.e.\ the term \isa{x\ {\isacharhash}\ y\ {\isacharhash}\ z} is read as \isa{x\ {\isacharhash}\ {\isacharparenleft}y\ {\isacharhash}\ z{\isacharparenright}}
+and not as \isa{{\isacharparenleft}x\ {\isacharhash}\ y{\isacharparenright}\ {\isacharhash}\ z}.
 
 \begin{warn}
   Syntax annotations are a powerful but completely optional feature. You
   could drop them from theory \isa{ToyList} and go back to the identifiers
-  \isa{Nil} and \isa{Cons}. However, lists are such a central datatype
+  \isa{Nil} and \isa{Cons}. However, lists are such a
+  central datatype
   that their syntax is highly customized. We recommend that novices should
   not use syntax annotations in their own theories.
 \end{warn}
@@ -46,9 +47,9 @@
 In contrast to ML, Isabelle insists on explicit declarations of all functions
 (keyword \isacommand{consts}).  (Apart from the declaration-before-use
 restriction, the order of items in a theory file is unconstrained.) Function
-\isa{app} is annotated with concrete syntax too. Instead of the prefix
+\isa{op\ {\isacharat}} is annotated with concrete syntax too. Instead of the prefix
 syntax \isa{app xs ys} the infix
-\isa{\mbox{xs}\ {\isacharat}\ \mbox{ys}}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
+\isa{xs\ {\isacharat}\ ys}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
 form. Both functions are defined recursively:%
 \end{isamarkuptext}%
 \isacommand{primrec}\isanewline
@@ -60,8 +61,8 @@
 {\isachardoublequote}rev\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ \ {\isacharequal}\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}x\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
-The equations for \isa{app} and \isa{rev} hardly need comments:
-\isa{app} appends two lists and \isa{rev} reverses a list.  The keyword
+The equations for \isa{op\ {\isacharat}} and \isa{rev} hardly need comments:
+\isa{op\ {\isacharat}} appends two lists and \isa{rev} reverses a list.  The keyword
 \isacommand{primrec}\index{*primrec} indicates that the recursion is of a
 particularly primitive kind where each recursive call peels off a datatype
 constructor from one of the arguments.  Thus the
@@ -110,7 +111,7 @@
 illustrate not just the basic proof commands but also the typical proof
 process.
 
-\subsubsection*{Main goal: \texttt{rev(rev xs) = xs}}
+\subsubsection*{Main goal: \isa{rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}}
 
 Our goal is to show that reversing a list twice produces the original
 list. The input line%
@@ -120,13 +121,14 @@
 \index{*theorem|bold}\index{*simp (attribute)|bold}
 \begin{itemize}
 \item
-establishes a new theorem to be proved, namely \isa{rev(rev xs) = xs},
-\item
-gives that theorem the name \isa{rev_rev} by which it can be referred to,
+establishes a new theorem to be proved, namely \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs},
 \item
-and tells Isabelle (via \isa{[simp]}) to use the theorem (once it has been
+gives that theorem the name \isa{rev{\isacharunderscore}rev} by which it can be
+referred to,
+\item
+and tells Isabelle (via \isa{{\isacharbrackleft}simp{\isacharbrackright}}) to use the theorem (once it has been
 proved) as a simplification rule, i.e.\ all future proofs involving
-simplification will replace occurrences of \isa{rev(rev xs)} by
+simplification will replace occurrences of \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}} by
 \isa{xs}.
 
 The name and the simplification attribute are optional.
@@ -140,7 +142,7 @@
 ~1.~rev~(rev~xs)~=~xs
 \end{isabelle}
 The first three lines tell us that we are 0 steps into the proof of
-theorem \isa{rev_rev}; for compactness reasons we rarely show these
+theorem \isa{rev{\isacharunderscore}rev}; for compactness reasons we rarely show these
 initial lines in this tutorial. The remaining lines display the current
 proof state.
 Until we have finished a proof, the proof state always looks like this:
@@ -153,11 +155,11 @@
 where $G$
 is the overall goal that we are trying to prove, and the numbered lines
 contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ that we need to prove to
-establish $G$. At \isa{step 0} there is only one subgoal, which is
+establish $G$. At \isa{step\ \isadigit{0}} there is only one subgoal, which is
 identical with the overall goal.  Normally $G$ is constant and only serves as
 a reminder. Hence we rarely show it in this tutorial.
 
-Let us now get back to \isa{rev(rev xs) = xs}. Properties of recursively
+Let us now get back to \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}. Properties of recursively
 defined functions are best established by induction. In this case there is
 not much choice except to induct on \isa{xs}:%
 \end{isamarkuptxt}%
@@ -171,7 +173,7 @@
 (\isa{Cons}):
 \begin{isabelle}
 ~1.~rev~(rev~[])~=~[]\isanewline
-~2.~{\isasymAnd}a~list.~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev(a~\#~list))~=~a~\#~list%
+~2.~{\isasymAnd}a~list.~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev(a~\#~list))~=~a~\#~list
 \end{isabelle}
 
 The induction step is an example of the general format of a subgoal:
@@ -184,12 +186,11 @@
 The {\it assumptions} are the local assumptions for this subgoal and {\it
   conclusion} is the actual proposition to be proved. Typical proof steps
 that add new assumptions are induction or case distinction. In our example
-the only assumption is the induction hypothesis \isa{rev\ {\isacharparenleft}rev\ \mbox{list}{\isacharparenright}\ {\isacharequal}\ \mbox{list}}, where \isa{list} is a variable name chosen by Isabelle. If there
+the only assumption is the induction hypothesis \isa{rev\ {\isacharparenleft}rev\ list{\isacharparenright}\ {\isacharequal}\ list}, where \isa{list} is a variable name chosen by Isabelle. If there
 are multiple assumptions, they are enclosed in the bracket pair
 \indexboldpos{\isasymlbrakk}{$Isabrl} and
 \indexboldpos{\isasymrbrakk}{$Isabrr} and separated by semicolons.
 
-%FIXME indent!
 Let us try to solve both goals automatically:%
 \end{isamarkuptxt}%
 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}%
@@ -198,7 +199,7 @@
 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
-to the equation \isa{rev [] = []}) and disappears; the simplified version
+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}
 ~1.~\dots~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev~list~@~a~\#~[])~=~a~\#~list
@@ -206,7 +207,7 @@
 In order to simplify this subgoal further, a lemma suggests itself.%
 \end{isamarkuptxt}%
 %
-\isamarkupsubsubsection{First lemma: \texttt{rev(xs \at~ys) = (rev ys) \at~(rev xs)}}
+\isamarkupsubsubsection{First lemma: \isa{rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}}}
 %
 \begin{isamarkuptext}%
 After abandoning the above proof attempt\indexbold{abandon
@@ -222,7 +223,7 @@
 interchangeably.
 
 There are two variables that we could induct on: \isa{xs} and
-\isa{ys}. Because \isa{\at} is defined by recursion on
+\isa{ys}. Because \isa{{\isacharat}} is defined by recursion on
 the first argument, \isa{xs} is the correct one:%
 \end{isamarkuptxt}%
 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}%
@@ -241,7 +242,7 @@
 the proof of a lemma usually remains implicit.%
 \end{isamarkuptxt}%
 %
-\isamarkupsubsubsection{Second lemma: \texttt{xs \at~[] = xs}}
+\isamarkupsubsubsection{Second lemma: \isa{xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs}}
 %
 \begin{isamarkuptext}%
 This time the canonical proof procedure%
@@ -251,7 +252,7 @@
 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}%
 \begin{isamarkuptxt}%
 \noindent
-leads to the desired message \isa{No subgoals!}:
+leads to the desired message \isa{No\ subgoals{\isacharbang}}:
 \begin{isabelle}
 xs~@~[]~=~xs\isanewline
 No~subgoals!
@@ -263,12 +264,12 @@
 \begin{isamarkuptext}%
 \noindent\indexbold{$Isar@\texttt{.}}%
 As a result of that final dot, Isabelle associates the lemma
-just proved with its name. Notice that in the lemma \isa{app_Nil2} (as
-printed out after the final dot) the free variable \isa{xs} has been
-replaced by the unknown \isa{?xs}, just as explained in
-\S\ref{sec:variables}. Note that instead of instead of \isacommand{apply}
+just proved with its name. Instead of \isacommand{apply}
 followed by a dot, you can simply write \isacommand{by}\indexbold{by},
-which we do most of the time.
+which we do most of the time. Notice that in lemma \isa{app{\isacharunderscore}Nil\isadigit{2}}
+(as printed out after the final dot) the free variable \isa{xs} has been
+replaced by the unknown \isa{{\isacharquery}xs}, just as explained in
+\S\ref{sec:variables}.
 
 Going back to the proof of the first lemma%
 \end{isamarkuptext}%
@@ -284,16 +285,16 @@
 ~~~~~~~rev~(list~@~ys)~=~rev~ys~@~rev~list~{\isasymLongrightarrow}\isanewline
 ~~~~~~~(rev~ys~@~rev~list)~@~a~\#~[]~=~rev~ys~@~rev~list~@~a~\#~[]
 \end{isabelle}
-Now we need to remember that \isa{\at} associates to the right, and that
-\isa{\#} and \isa{\at} have the same priority (namely the \isa{65}
+Now we need to remember that \isa{{\isacharat}} associates to the right, and that
+\isa{{\isacharhash}} and \isa{{\isacharat}} have the same priority (namely the \isa{\isadigit{6}\isadigit{5}}
 in their \isacommand{infixr} annotation). Thus the conclusion really is
 \begin{isabelle}
-~~~~~(rev~ys~@~rev~list)~@~(a~\#~[])~=~rev~ys~@~(rev~list~@~(a~\#~[]))%
+~~~~~(rev~ys~@~rev~list)~@~(a~\#~[])~=~rev~ys~@~(rev~list~@~(a~\#~[]))
 \end{isabelle}
-and the missing lemma is associativity of \isa{\at}.%
+and the missing lemma is associativity of \isa{{\isacharat}}.%
 \end{isamarkuptxt}%
 %
-\isamarkupsubsubsection{Third lemma: \texttt{(xs \at~ys) \at~zs = xs \at~(ys \at~zs)}}
+\isamarkupsubsubsection{Third lemma: \isa{{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}}}
 %
 \begin{isamarkuptext}%
 Abandoning the previous proof, the canonical proof procedure%
@@ -318,7 +319,7 @@
 \isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
-The final \isa{end} tells Isabelle to close the current theory because
+The final \isacommand{end} tells Isabelle to close the current theory because
 we are finished with its development:%
 \end{isamarkuptext}%
 \isacommand{end}\isanewline




