diff -r 2c208c98f541 -r 1b2d4f995b13 doc-src/TutorialI/Misc/document/AdvancedInd.tex
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Mon Aug 21 19:03:58 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Mon Aug 21 19:17:07 2000 +0200
@@ -15,8 +15,8 @@
 So far we have assumed that the theorem we want to prove is already in a form
 that is amenable to induction, but this is not always the case:%
 \end{isamarkuptext}%
-\isacommand{lemma}\ {"}xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd(rev\ xs)\ =\ last\ xs{"}\isanewline
-\isacommand{apply}(induct\_tac\ xs)%
+\isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}\isanewline
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}%
 \begin{isamarkuptxt}%
 \noindent
 (where \isa{hd} and \isa{last} return the first and last element of a
@@ -46,7 +46,7 @@
 \end{quote}
 This means we should prove%
 \end{isamarkuptxt}%
-\isacommand{lemma}\ hd\_rev:\ {"}xs\ {\isasymnoteq}\ []\ {\isasymlongrightarrow}\ hd(rev\ xs)\ =\ last\ xs{"}%
+\isacommand{lemma}\ hd{\isacharunderscore}rev{\isacharcolon}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 This time, induction leaves us with the following base case
@@ -60,7 +60,7 @@
 example because you want to apply it as an introduction rule, you need to
 derive it separately, by combining it with modus ponens:%
 \end{isamarkuptext}%
-\isacommand{lemmas}\ hd\_revI\ =\ hd\_rev[THEN\ mp]%
+\isacommand{lemmas}\ hd{\isacharunderscore}revI\ {\isacharequal}\ hd{\isacharunderscore}rev{\isacharbrackleft}THEN\ mp{\isacharbrackright}%
 \begin{isamarkuptext}%
 \noindent
 which yields the lemma we originally set out to prove.
@@ -73,26 +73,26 @@
 which can yield a fairly complex conclusion.
 Here is a simple example (which is proved by \isa{blast}):%
 \end{isamarkuptext}%
-\isacommand{lemma}\ simple:\ {"}{\isasymforall}\ y.\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ \&\ A\ y{"}%
+\isacommand{lemma}\ simple{\isacharcolon}\ {\isachardoublequote}{\isasymforall}\ y{\isachardot}\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ {\isacharampersand}\ A\ y{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 You can get the desired lemma by explicit
 application of modus ponens and \isa{spec}:%
 \end{isamarkuptext}%
-\isacommand{lemmas}\ myrule\ =\ simple[THEN\ spec,\ THEN\ mp,\ THEN\ mp]%
+\isacommand{lemmas}\ myrule\ {\isacharequal}\ simple{\isacharbrackleft}THEN\ spec{\isacharcomma}\ THEN\ mp{\isacharcomma}\ THEN\ mp{\isacharbrackright}%
 \begin{isamarkuptext}%
 \noindent
 or the wholesale stripping of \isa{\isasymforall} and
 \isa{\isasymlongrightarrow} in the conclusion via \isa{rulify}%
 \end{isamarkuptext}%
-\isacommand{lemmas}\ myrule\ =\ simple[rulify]%
+\isacommand{lemmas}\ myrule\ {\isacharequal}\ simple{\isacharbrackleft}rulify{\isacharbrackright}%
 \begin{isamarkuptext}%
 \noindent
-yielding \isa{{\isasymlbrakk}\mbox{?A}\ \mbox{?y};\ \mbox{?B}\ \mbox{?y}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{?B}\ \mbox{?y}\ {\isasymand}\ \mbox{?A}\ \mbox{?y}}.
+yielding \isa{{\isasymlbrakk}\mbox{{\isacharquery}A}\ \mbox{{\isacharquery}y}{\isacharsemicolon}\ \mbox{{\isacharquery}B}\ \mbox{{\isacharquery}y}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{{\isacharquery}B}\ \mbox{{\isacharquery}y}\ {\isasymand}\ \mbox{{\isacharquery}A}\ \mbox{{\isacharquery}y}}.
 You can go one step further and include these derivations already in the
 statement of your original lemma, thus avoiding the intermediate step:%
 \end{isamarkuptext}%
-\isacommand{lemma}\ myrule[rulify]:\ \ {"}{\isasymforall}\ y.\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ \&\ A\ y{"}%
+\isacommand{lemma}\ myrule{\isacharbrackleft}rulify{\isacharbrackright}{\isacharcolon}\ \ {\isachardoublequote}{\isasymforall}\ y{\isachardot}\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ {\isacharampersand}\ A\ y{\isachardoublequote}%
 \begin{isamarkuptext}%
 \bigskip
 
@@ -121,14 +121,14 @@
 \begin{quote}
 
 \begin{isabelle}%
-({\isasymAnd}\mbox{n}.\ {\isasymforall}\mbox{m}.\ \mbox{m}\ <\ \mbox{n}\ {\isasymlongrightarrow}\ \mbox{?P}\ \mbox{m}\ {\isasymLongrightarrow}\ \mbox{?P}\ \mbox{n})\ {\isasymLongrightarrow}\ \mbox{?P}\ \mbox{?n}
+{\isacharparenleft}{\isasymAnd}\mbox{n}{\isachardot}\ {\isasymforall}\mbox{m}{\isachardot}\ \mbox{m}\ {\isacharless}\ \mbox{n}\ {\isasymlongrightarrow}\ \mbox{{\isacharquery}P}\ \mbox{m}\ {\isasymLongrightarrow}\ \mbox{{\isacharquery}P}\ \mbox{n}{\isacharparenright}\ {\isasymLongrightarrow}\ \mbox{{\isacharquery}P}\ \mbox{{\isacharquery}n}
 \end{isabelle}%
 
 \end{quote}
 Here is an example of its application.%
 \end{isamarkuptext}%
-\isacommand{consts}\ f\ ::\ {"}nat\ =>\ nat{"}\isanewline
-\isacommand{axioms}\ f\_ax:\ {"}f(f(n))\ <\ f(Suc(n)){"}%
+\isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isacharequal}{\isachargreater}\ nat{\isachardoublequote}\isanewline
+\isacommand{axioms}\ f{\isacharunderscore}ax{\isacharcolon}\ {\isachardoublequote}f{\isacharparenleft}f{\isacharparenleft}n{\isacharparenright}{\isacharparenright}\ {\isacharless}\ f{\isacharparenleft}Suc{\isacharparenleft}n{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 From the above axiom\footnote{In general, the use of axioms is strongly
@@ -139,14 +139,14 @@
 be proved by induction on \isa{f\ \mbox{n}}. Following the recipy outlined
 above, we have to phrase the proposition as follows to allow induction:%
 \end{isamarkuptext}%
-\isacommand{lemma}\ f\_incr\_lem:\ {"}{\isasymforall}i.\ k\ =\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{"}%
+\isacommand{lemma}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}%
 \begin{isamarkuptxt}%
 \noindent
 To perform induction on \isa{k} using \isa{less\_induct}, we use the same
 general induction method as for recursion induction (see
 \S\ref{sec:recdef-induction}):%
 \end{isamarkuptxt}%
-\isacommand{apply}(induct\_tac\ k\ rule:less\_induct)%
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ k\ rule{\isacharcolon}less{\isacharunderscore}induct{\isacharparenright}%
 \begin{isamarkuptxt}%
 \noindent
 which leaves us with the following proof state:
@@ -163,19 +163,19 @@
 \ \ \ \ \ \ \ {\isasymLongrightarrow}\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i}
 \end{isabellepar}%%
 \end{isamarkuptxt}%
-\isacommand{by}(blast\ intro!:\ f\_ax\ Suc\_leI\ intro:le\_less\_trans)%
+\isacommand{by}{\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ f{\isacharunderscore}ax\ Suc{\isacharunderscore}leI\ intro{\isacharcolon}le{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
 It is not surprising if you find the last step puzzling.
 The proof goes like this (writing \isa{j} instead of \isa{nat}).
-Since \isa{\mbox{i}\ =\ Suc\ \mbox{j}} it suffices to show
-\isa{\mbox{j}\ <\ f\ (Suc\ \mbox{j})} (by \isa{Suc\_leI}: \isa{\mbox{?m}\ <\ \mbox{?n}\ {\isasymLongrightarrow}\ Suc\ \mbox{?m}\ {\isasymle}\ \mbox{?n}}). This is
-proved as follows. From \isa{f\_ax} we have \isa{f\ (f\ \mbox{j})\ <\ f\ (Suc\ \mbox{j})}
-(1) which implies \isa{f\ \mbox{j}\ {\isasymle}\ f\ (f\ \mbox{j})} (by the induction hypothesis).
-Using (1) once more we obtain \isa{f\ \mbox{j}\ <\ f\ (Suc\ \mbox{j})} (2) by transitivity
-(\isa{le_less_trans}: \isa{{\isasymlbrakk}\mbox{?i}\ {\isasymle}\ \mbox{?j};\ \mbox{?j}\ <\ \mbox{?k}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{?i}\ <\ \mbox{?k}}).
+Since \isa{\mbox{i}\ {\isacharequal}\ Suc\ \mbox{j}} it suffices to show
+\isa{\mbox{j}\ {\isacharless}\ f\ {\isacharparenleft}Suc\ \mbox{j}{\isacharparenright}} (by \isa{Suc\_leI}: \isa{\mbox{{\isacharquery}m}\ {\isacharless}\ \mbox{{\isacharquery}n}\ {\isasymLongrightarrow}\ Suc\ \mbox{{\isacharquery}m}\ {\isasymle}\ \mbox{{\isacharquery}n}}). This is
+proved as follows. From \isa{f\_ax} we have \isa{f\ {\isacharparenleft}f\ \mbox{j}{\isacharparenright}\ {\isacharless}\ f\ {\isacharparenleft}Suc\ \mbox{j}{\isacharparenright}}
+(1) which implies \isa{f\ \mbox{j}\ {\isasymle}\ f\ {\isacharparenleft}f\ \mbox{j}{\isacharparenright}} (by the induction hypothesis).
+Using (1) once more we obtain \isa{f\ \mbox{j}\ {\isacharless}\ f\ {\isacharparenleft}Suc\ \mbox{j}{\isacharparenright}} (2) by transitivity
+(\isa{le_less_trans}: \isa{{\isasymlbrakk}\mbox{{\isacharquery}i}\ {\isasymle}\ \mbox{{\isacharquery}j}{\isacharsemicolon}\ \mbox{{\isacharquery}j}\ {\isacharless}\ \mbox{{\isacharquery}k}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{{\isacharquery}i}\ {\isacharless}\ \mbox{{\isacharquery}k}}).
 Using the induction hypothesis once more we obtain \isa{\mbox{j}\ {\isasymle}\ f\ \mbox{j}}
-which, together with (2) yields \isa{\mbox{j}\ <\ f\ (Suc\ \mbox{j})} (again by
+which, together with (2) yields \isa{\mbox{j}\ {\isacharless}\ f\ {\isacharparenleft}Suc\ \mbox{j}{\isacharparenright}} (again by
 \isa{le_less_trans}).
 
 This last step shows both the power and the danger of automatic proofs: they
@@ -186,12 +186,12 @@
 
 We can now derive the desired \isa{\mbox{i}\ {\isasymle}\ f\ \mbox{i}} from \isa{f\_incr}:%
 \end{isamarkuptext}%
-\isacommand{lemmas}\ f\_incr\ =\ f\_incr\_lem[rulify,\ OF\ refl]%
+\isacommand{lemmas}\ f{\isacharunderscore}incr\ {\isacharequal}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharbrackleft}rulify{\isacharcomma}\ OF\ refl{\isacharbrackright}%
 \begin{isamarkuptext}%
 The final \isa{refl} gets rid of the premise \isa{?k = f ?i}. Again, we could
 have included this derivation in the original statement of the lemma:%
 \end{isamarkuptext}%
-\isacommand{lemma}\ f\_incr[rulify,\ OF\ refl]:\ {"}{\isasymforall}i.\ k\ =\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{"}%
+\isacommand{lemma}\ f{\isacharunderscore}incr{\isacharbrackleft}rulify{\isacharcomma}\ OF\ refl{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}%
 \begin{isamarkuptext}%
 \begin{exercise}
 From the above axiom and lemma for \isa{f} show that \isa{f} is the identity.
@@ -216,7 +216,7 @@
 \begin{quote}
 
 \begin{isabelle}%
-{\isasymlbrakk}wf\ \mbox{?r};\ {\isasymAnd}\mbox{x}.\ {\isasymforall}\mbox{y}.\ (\mbox{y},\ \mbox{x})\ {\isasymin}\ \mbox{?r}\ {\isasymlongrightarrow}\ \mbox{?P}\ \mbox{y}\ {\isasymLongrightarrow}\ \mbox{?P}\ \mbox{x}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{?P}\ \mbox{?a}
+{\isasymlbrakk}wf\ \mbox{{\isacharquery}r}{\isacharsemicolon}\ {\isasymAnd}\mbox{x}{\isachardot}\ {\isasymforall}\mbox{y}{\isachardot}\ {\isacharparenleft}\mbox{y}{\isacharcomma}\ \mbox{x}{\isacharparenright}\ {\isasymin}\ \mbox{{\isacharquery}r}\ {\isasymlongrightarrow}\ \mbox{{\isacharquery}P}\ \mbox{y}\ {\isasymLongrightarrow}\ \mbox{{\isacharquery}P}\ \mbox{x}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{{\isacharquery}P}\ \mbox{{\isacharquery}a}
 \end{isabelle}%
 
 \end{quote}