updated;

--- a/doc-src/TutorialI/Datatype/document/ABexpr.tex	Mon Aug 28 14:09:33 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex	Mon Aug 28 15:13:55 2000 +0200
@@ -91,7 +91,7 @@
 \noindent
 The resulting 8 goals (one for each constructor) are proved in one fell swoop:%
 \end{isamarkuptxt}%
-\isacommand{by}\ simp\_all%
+\isacommand{by}\ simp{\isacharunderscore}all%
 \begin{isamarkuptext}%
 In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$,
 an inductive proof expects a goal of the form

--- a/doc-src/TutorialI/Datatype/document/Fundata.tex	Mon Aug 28 14:09:33 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Fundata.tex	Mon Aug 28 15:13:55 2000 +0200
@@ -37,7 +37,7 @@
 The following lemma has a canonical proof%
 \end{isamarkuptext}%
 \isacommand{lemma}\ {\isachardoublequote}map{\isacharunderscore}bt\ {\isacharparenleft}g\ o\ f{\isacharparenright}\ T\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ T{\isacharparenright}{\isachardoublequote}\isanewline
-\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ {\isachardoublequote}T{\isachardoublequote}{\isacharcomma}\ auto{\isacharparenright}%
+\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ {\isachardoublequote}T{\isachardoublequote}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
 but it is worth taking a look at the proof state after the induction step

--- a/doc-src/TutorialI/Datatype/document/Nested.tex	Mon Aug 28 14:09:33 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex	Mon Aug 28 15:13:55 2000 +0200
@@ -6,14 +6,14 @@
 constructor. This is not the case any longer for the following model of terms
 where function symbols can be applied to a list of arguments:%
 \end{isamarkuptext}%
-\isacommand{datatype}\ ('a,'b){"}term{"}\ =\ Var\ 'a\ |\ App\ 'b\ {"}('a,'b)term\ list{"}%
+\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}{\isachardoublequote}term{\isachardoublequote}\ {\isacharequal}\ Var\ {\isacharprime}a\ {\isacharbar}\ App\ {\isacharprime}b\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ list{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 Note that we need to quote \isa{term} on the left to avoid confusion with
 the command \isacommand{term}.
 Parameter \isa{'a} is the type of variables and \isa{'b} the type of
 function symbols.
-A mathematical term like $f(x,g(y))$ becomes \isa{App\ \mbox{f}\ [Var\ \mbox{x},\ App\ \mbox{g}\ [Var\ \mbox{y}]]}, where \isa{f}, \isa{g}, \isa{x}, \isa{y} are
+A mathematical term like $f(x,g(y))$ becomes \isa{App\ \mbox{f}\ {\isacharbrackleft}Var\ \mbox{x}{\isacharcomma}\ App\ \mbox{g}\ {\isacharbrackleft}Var\ \mbox{y}{\isacharbrackright}{\isacharbrackright}}, where \isa{f}, \isa{g}, \isa{x}, \isa{y} are
 suitable values, e.g.\ numbers or strings.
 
 What complicates the definition of \isa{term} is the nested occurrence of
@@ -36,16 +36,16 @@
 lists, we need to define two substitution functions simultaneously:%
 \end{isamarkuptext}%
 \isacommand{consts}\isanewline
-subst\ ::\ {"}('a{\isasymRightarrow}('a,'b)term)\ {\isasymRightarrow}\ ('a,'b)term\ \ \ \ \ \ {\isasymRightarrow}\ ('a,'b)term{"}\isanewline
-substs::\ {"}('a{\isasymRightarrow}('a,'b)term)\ {\isasymRightarrow}\ ('a,'b)term\ list\ {\isasymRightarrow}\ ('a,'b)term\ list{"}\isanewline
+subst\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isasymRightarrow}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ \ \ \ \ \ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}\isanewline
+substs{\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isasymRightarrow}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ list{\isachardoublequote}\isanewline
 \isanewline
 \isacommand{primrec}\isanewline
-\ \ {"}subst\ s\ (Var\ x)\ =\ s\ x{"}\isanewline
-\ \ subst\_App:\isanewline
-\ \ {"}subst\ s\ (App\ f\ ts)\ =\ App\ f\ (substs\ s\ ts){"}\isanewline
+\ \ {\isachardoublequote}subst\ s\ {\isacharparenleft}Var\ x{\isacharparenright}\ {\isacharequal}\ s\ x{\isachardoublequote}\isanewline
+\ \ subst{\isacharunderscore}App{\isacharcolon}\isanewline
+\ \ {\isachardoublequote}subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}substs\ s\ ts{\isacharparenright}{\isachardoublequote}\isanewline
 \isanewline
-\ \ {"}substs\ s\ []\ =\ []{"}\isanewline
-\ \ {"}substs\ s\ (t\ \#\ ts)\ =\ subst\ s\ t\ \#\ substs\ s\ ts{"}%
+\ \ {\isachardoublequote}substs\ s\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}substs\ s\ {\isacharparenleft}t\ {\isacharhash}\ ts{\isacharparenright}\ {\isacharequal}\ subst\ s\ t\ {\isacharhash}\ substs\ s\ ts{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 You should ignore the label \isa{subst\_App} for the moment.
@@ -55,13 +55,13 @@
 the fact that the identity substitution does not change a term needs to be
 strengthened and proved as follows:%
 \end{isamarkuptext}%
-\isacommand{lemma}\ {"}subst\ \ Var\ t\ \ =\ (t\ ::('a,'b)term)\ \ {\isasymand}\isanewline
-\ \ \ \ \ \ \ \ substs\ Var\ ts\ =\ (ts::('a,'b)term\ list){"}\isanewline
-\isacommand{by}(induct\_tac\ t\ \isakeyword{and}\ ts,\ simp\_all)%
+\isacommand{lemma}\ {\isachardoublequote}subst\ \ Var\ t\ \ {\isacharequal}\ {\isacharparenleft}t\ {\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharparenright}\ \ {\isasymand}\isanewline
+\ \ \ \ \ \ \ \ substs\ Var\ ts\ {\isacharequal}\ {\isacharparenleft}ts{\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ list{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ \isakeyword{and}\ ts{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
 Note that \isa{Var} is the identity substitution because by definition it
-leaves variables unchanged: \isa{subst\ Var\ (Var\ \mbox{x})\ =\ Var\ \mbox{x}}. Note also
+leaves variables unchanged: \isa{subst\ Var\ {\isacharparenleft}Var\ \mbox{x}{\isacharparenright}\ {\isacharequal}\ Var\ \mbox{x}}. Note also
 that the type annotations are necessary because otherwise there is nothing in
 the goal to enforce that both halves of the goal talk about the same type
 parameters \isa{('a,'b)}. As a result, induction would fail
@@ -78,7 +78,7 @@
 its definition is found in theorem \isa{o_def}).
 \end{exercise}
 \begin{exercise}\label{ex:trev-trev}
-  Define a function \isa{trev} of type \isa{(\mbox{'a},\ \mbox{'b})\ term\ {\isasymRightarrow}\ (\mbox{'a},\ \mbox{'b})\ term} that
+  Define a function \isa{trev} of type \isa{{\isacharparenleft}\mbox{{\isacharprime}a}{\isacharcomma}\ \mbox{{\isacharprime}b}{\isacharparenright}\ term\ {\isasymRightarrow}\ {\isacharparenleft}\mbox{{\isacharprime}a}{\isacharcomma}\ \mbox{{\isacharprime}b}{\isacharparenright}\ term} that
   recursively reverses the order of arguments of all function symbols in a
   term. Prove that \isa{trev(trev t) = t}.
 \end{exercise}
@@ -89,7 +89,7 @@
 \begin{quote}
 
 \begin{isabelle}%
-subst\ \mbox{s}\ (App\ \mbox{f}\ \mbox{ts})\ =\ App\ \mbox{f}\ (map\ (subst\ \mbox{s})\ \mbox{ts})
+subst\ \mbox{s}\ {\isacharparenleft}App\ \mbox{f}\ \mbox{ts}{\isacharparenright}\ {\isacharequal}\ App\ \mbox{f}\ {\isacharparenleft}map\ {\isacharparenleft}subst\ \mbox{s}{\isacharparenright}\ \mbox{ts}{\isacharparenright}
 \end{isabelle}%
 
 \end{quote}
@@ -98,14 +98,14 @@
 on the above fixed format. Fortunately, we can easily \emph{prove} that the
 suggested equation holds:%
 \end{isamarkuptext}%
-\isacommand{lemma}\ [simp]:\ {"}subst\ s\ (App\ f\ ts)\ =\ App\ f\ (map\ (subst\ s)\ ts){"}\isanewline
-\isacommand{by}(induct\_tac\ ts,\ simp\_all)%
+\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}map\ {\isacharparenleft}subst\ s{\isacharparenright}\ ts{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ ts{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
 What is more, we can now disable the old defining equation as a
 simplification rule:%
 \end{isamarkuptext}%
-\isacommand{lemmas}\ [simp\ del]\ =\ subst\_App%
+\isacommand{lemmas}\ {\isacharbrackleft}simp\ del{\isacharbrackright}\ {\isacharequal}\ subst{\isacharunderscore}App%
 \begin{isamarkuptext}%
 \noindent
 The advantage is that now we have replaced \isa{substs} by

--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Mon Aug 28 14:09:33 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Mon Aug 28 15:13:55 2000 +0200
@@ -55,7 +55,7 @@
 \end{isabellepar}%
 which is trivial, and \isa{auto} finishes the whole proof.
 
-If \isa{hd\_rev} is meant to be simplification rule, you are done. But if you
+If \isa{hd\_rev} is meant to be a simplification rule, you are done. But if you
 really need the \isa{\isasymLongrightarrow}-version of \isa{hd\_rev}, for
 example because you want to apply it as an introduction rule, you need to
 derive it separately, by combining it with modus ponens:%
@@ -73,7 +73,7 @@
 which can yield a fairly complex conclusion.
 Here is a simple example (which is proved by \isa{blast}):%
 \end{isamarkuptext}%
-\isacommand{lemma}\ simple{\isacharcolon}\ {\isachardoublequote}{\isasymforall}\ y{\isachardot}\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ {\isacharampersand}\ A\ y{\isachardoublequote}%
+\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
@@ -88,11 +88,11 @@
 \isacommand{lemmas}\ myrule\ {\isacharequal}\ simple{\isacharbrackleft}rulify{\isacharbrackright}%
 \begin{isamarkuptext}%
 \noindent
-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}}.
+yielding \isa{{\isasymlbrakk}\mbox{A}\ \mbox{y}{\isacharsemicolon}\ \mbox{B}\ \mbox{y}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{B}\ \mbox{y}\ {\isasymand}\ \mbox{A}\ \mbox{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{\isacharbrackleft}rulify{\isacharbrackright}{\isacharcolon}\ \ {\isachardoublequote}{\isasymforall}\ y{\isachardot}\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ {\isacharampersand}\ A\ y{\isachardoublequote}%
+\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
 
@@ -104,7 +104,7 @@
 afterwards. An example appears below.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsection{Beyond structural induction}
+\isamarkupsubsection{Beyond structural and recursion induction}
 %
 \begin{isamarkuptext}%
 So far, inductive proofs where by structural induction for
@@ -121,7 +121,7 @@
 \begin{quote}
 
 \begin{isabelle}%
-{\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}
+{\isacharparenleft}{\isasymAnd}\mbox{n}{\isachardot}\ {\isasymforall}\mbox{m}{\isachardot}\ \mbox{m}\ {\isacharless}\ \mbox{n}\ {\isasymlongrightarrow}\ \mbox{P}\ \mbox{m}\ {\isasymLongrightarrow}\ \mbox{P}\ \mbox{n}{\isacharparenright}\ {\isasymLongrightarrow}\ \mbox{P}\ \mbox{n}
 \end{isabelle}%
 
 \end{quote}
@@ -169,11 +169,11 @@
 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}\ {\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
+\isa{\mbox{j}\ {\isacharless}\ f\ {\isacharparenleft}Suc\ \mbox{j}{\isacharparenright}} (by \isa{Suc\_leI}: \isa{\mbox{m}\ {\isacharless}\ \mbox{n}\ {\isasymLongrightarrow}\ Suc\ \mbox{m}\ {\isasymle}\ \mbox{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}}).
+(\isa{le_less_trans}: \isa{{\isasymlbrakk}\mbox{i}\ {\isasymle}\ \mbox{j}{\isacharsemicolon}\ \mbox{j}\ {\isacharless}\ \mbox{k}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{i}\ {\isacharless}\ \mbox{k}}).
 Using the induction hypothesis once more we obtain \isa{\mbox{j}\ {\isasymle}\ f\ \mbox{j}}
 which, together with (2) yields \isa{\mbox{j}\ {\isacharless}\ f\ {\isacharparenleft}Suc\ \mbox{j}{\isacharparenright}} (again by
 \isa{le_less_trans}).
@@ -188,6 +188,7 @@
 \end{isamarkuptext}%
 \isacommand{lemmas}\ f{\isacharunderscore}incr\ {\isacharequal}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharbrackleft}rulify{\isacharcomma}\ OF\ refl{\isacharbrackright}%
 \begin{isamarkuptext}%
+\noindent
 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}%
@@ -209,17 +210,65 @@
 which case the application is
 \begin{ttbox}
 apply(induct_tac y1 ... yn and ... and z1 ... zm rule: r)
-\end{ttbox}
+\end{ttbox}%
+\end{isamarkuptext}%
+%
+\isamarkupsubsection{Derivation of new induction schemas}
+%
+\begin{isamarkuptext}%
+\label{sec:derive-ind}
+Induction schemas are ordinary theorems and you can derive new ones
+whenever you wish.  This section shows you how to, using the example
+of \isa{less\_induct}. Assume we only have structural induction
+available for \isa{nat} and want to derive complete induction. This
+requires us to generalize the statement first:%
+\end{isamarkuptext}%
+\isacommand{lemma}\ induct{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isasymAnd}n{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isacharequal}{\isacharequal}{\isachargreater}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m{\isachardoublequote}\isanewline
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}%
+\begin{isamarkuptxt}%
+\noindent
+The base case is trivially true. For the induction step (\isa{\mbox{m}\ {\isacharless}\ Suc\ \mbox{n}}) we distinguish two cases: \isa{\mbox{m}\ {\isacharless}\ \mbox{n}} is true by induction
+hypothesis and \isa{\mbox{m}\ {\isacharequal}\ \mbox{n}} follow from the assumption again using
+the induction hypothesis:%
+\end{isamarkuptxt}%
+\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
+\isanewline
+\isacommand{ML}{\isachardoublequote}set\ quick{\isacharunderscore}and{\isacharunderscore}dirty{\isachardoublequote}\isanewline
+\isacommand{sorry}\isanewline
+\isacommand{ML}{\isachardoublequote}reset\ quick{\isacharunderscore}and{\isacharunderscore}dirty{\isachardoublequote}%
+\begin{isamarkuptext}%
+\noindent
+The elimination rule \isa{less_SucE} expresses the case distinction:
+\begin{quote}
 
+\begin{isabelle}%
+{\isasymlbrakk}\mbox{m}\ {\isacharless}\ Suc\ \mbox{n}{\isacharsemicolon}\ \mbox{m}\ {\isacharless}\ \mbox{n}\ {\isasymLongrightarrow}\ \mbox{P}{\isacharsemicolon}\ \mbox{m}\ {\isacharequal}\ \mbox{n}\ {\isasymLongrightarrow}\ \mbox{P}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{P}
+\end{isabelle}%
+
+\end{quote}
+
+Now it is straightforward to derive the original version of
+\isa{less\_induct} by manipulting the conclusion of the above lemma:
+instantiate \isa{n} by \isa{Suc\ \mbox{n}} and \isa{m} by \isa{n} and
+remove the trivial condition \isa{\mbox{n}\ {\isacharless}\ \mbox{Sc}\ \mbox{n}}. Fortunately, this
+happens automatically when we add the lemma as a new premise to the
+desired goal:%
+\end{isamarkuptext}%
+\isacommand{theorem}\ less{\isacharunderscore}induct{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isasymAnd}n{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isacharequal}{\isacharequal}{\isachargreater}\ P\ n{\isachardoublequote}\isanewline
+\isacommand{by}{\isacharparenleft}insert\ induct{\isacharunderscore}lem{\isacharcomma}\ blast{\isacharparenright}%
+\begin{isamarkuptext}%
+\noindent
 Finally we should mention that HOL already provides the mother of all
 inductions, \emph{wellfounded induction} (\isa{wf\_induct}):
 \begin{quote}
 
 \begin{isabelle}%
-{\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}
+{\isasymlbrakk}wf\ \mbox{r}{\isacharsemicolon}\ {\isasymAnd}\mbox{x}{\isachardot}\ {\isasymforall}\mbox{y}{\isachardot}\ {\isacharparenleft}\mbox{y}{\isacharcomma}\ \mbox{x}{\isacharparenright}\ {\isasymin}\ \mbox{r}\ {\isasymlongrightarrow}\ \mbox{P}\ \mbox{y}\ {\isasymLongrightarrow}\ \mbox{P}\ \mbox{x}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{P}\ \mbox{a}
 \end{isabelle}%
 
 \end{quote}
+where \isa{wf\ \mbox{r}} means that the relation \isa{r} is wellfounded.
+For example \isa{less\_induct} is the special case where \isa{r} is \isa{<} on \isa{nat}.
 For details see the library.%
 \end{isamarkuptext}%
 \end{isabelle}%

--- a/doc-src/TutorialI/Misc/document/Itrev.tex	Mon Aug 28 14:09:33 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex	Mon Aug 28 15:13:55 2000 +0200
@@ -26,7 +26,7 @@
 \noindent
 There is no choice as to the induction variable, and we immediately simplify:%
 \end{isamarkuptxt}%
-\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ auto{\isacharparenright}%
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
 \begin{isamarkuptxt}%
 \noindent
 Unfortunately, this is not a complete success:

--- a/doc-src/TutorialI/Misc/document/def_rewr.tex	Mon Aug 28 14:09:33 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/def_rewr.tex	Mon Aug 28 15:13:55 2000 +0200
@@ -18,25 +18,22 @@
 \isacommand{lemma}\ {\isachardoublequote}exor\ A\ {\isacharparenleft}{\isasymnot}A{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptxt}%
 \noindent
-There is a special method for \emph{unfolding} definitions, which we need to
-get started:\indexbold{*unfold}\indexbold{definition!unfolding}%
+Typically, the opening move consists in \emph{unfolding} the definition(s), which we need to
+get started, but nothing else:\indexbold{*unfold}\indexbold{definition!unfolding}%
 \end{isamarkuptxt}%
-\isacommand{apply}{\isacharparenleft}unfold\ exor{\isacharunderscore}def{\isacharparenright}%
+\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}exor{\isacharunderscore}def{\isacharparenright}%
 \begin{isamarkuptxt}%
 \noindent
-It unfolds the given list of definitions (here merely one) in all subgoals:
+In this particular case, the resulting goal
 \begin{isabellepar}%
 ~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A%
 \end{isabellepar}%
-The resulting goal can be proved by simplification.
-
-In case we want to expand a definition in the middle of a proof, we can
-simply include it locally:%
+can be proved by simplification. Thus we could have proved the lemma outright%
 \end{isamarkuptxt}%
-\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ exor{\isacharunderscore}def{\isacharparenright}%
+\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ exor{\isacharunderscore}def{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
-In fact, this one command proves the above lemma directly.
+Of course we can also unfold definitions in the middle of a proof.
 
 You should normally not turn a definition permanently into a simplification
 rule because this defeats the whole purpose of an abbreviation.%

--- a/doc-src/TutorialI/Recdef/document/Induction.tex	Mon Aug 28 14:09:33 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Induction.tex	Mon Aug 28 15:13:55 2000 +0200
@@ -36,7 +36,7 @@
 \end{isabellepar}%
 The rest is pure simplification:%
 \end{isamarkuptxt}%
-\isacommand{by}\ simp\_all%
+\isacommand{by}\ simp{\isacharunderscore}all%
 \begin{isamarkuptext}%
 Try proving the above lemma by structural induction, and you find that you
 need an additional case distinction. What is worse, the names of variables

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Recdef/document/Nested0.tex	Mon Aug 28 15:13:55 2000 +0200
@@ -0,0 +1,23 @@
+\begin{isabelle}%
+%
+\begin{isamarkuptext}%
+In \S\ref{sec:nested-datatype} we defined the datatype of terms%
+\end{isamarkuptext}%
+\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}{\isachardoublequote}term{\isachardoublequote}\ {\isacharequal}\ Var\ {\isacharprime}a\ {\isacharbar}\ App\ {\isacharprime}b\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ list{\isachardoublequote}%
+\begin{isamarkuptext}%
+\noindent
+and closed with the observation that the associated schema for the definition
+of primitive recursive functions leads to overly verbose definitions. Moreover,
+if you have worked exercise~\ref{ex:trev-trev} you will have noticed that
+you needed to reprove many lemmas reminiscent of similar lemmas about
+\isa{rev}. We will now show you how \isacommand{recdef} can simplify
+definitions and proofs about nested recursive datatypes. As an example we
+chose exercise~\ref{ex:trev-trev}:
+
+FIXME: declare trev now!%
+\end{isamarkuptext}%
+\end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Recdef/document/Nested1.tex	Mon Aug 28 15:13:55 2000 +0200
@@ -0,0 +1,45 @@
+\begin{isabelle}%
+\isacommand{consts}\ trev\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ {\isacharequal}{\isachargreater}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}%
+\begin{isamarkuptext}%
+\noindent
+Although the definition of \isa{trev} is quite natural, we will have
+overcome a minor difficulty in convincing Isabelle of is termination.
+It is precisely this difficulty that is the \textit{rasion d'\^etre} of
+this subsection.
+
+Defining \isa{trev} by \isacommand{recdef} rather than \isacommand{primrec}
+simplifies matters because we are now free to use the recursion equation
+suggested at the end of \S\ref{sec:nested-datatype}:%
+\end{isamarkuptext}%
+\isacommand{recdef}\ trev\ {\isachardoublequote}measure\ size{\isachardoublequote}\isanewline
+\ {\isachardoublequote}trev\ {\isacharparenleft}Var\ x{\isacharparenright}\ {\isacharequal}\ Var\ x{\isachardoublequote}\isanewline
+\ {\isachardoublequote}trev\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}rev{\isacharparenleft}map\ trev\ ts{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
+\begin{isamarkuptext}%
+FIXME: recdef should complain and generate unprovable termination condition!
+moveto todo
+
+Remember that function \isa{size} is defined for each \isacommand{datatype}.
+However, the definition does not succeed. Isabelle complains about an unproved termination
+condition
+\begin{quote}
+
+\begin{isabelle}%
+\mbox{t}\ {\isasymin}\ set\ \mbox{ts}\ {\isasymlongrightarrow}\ size\ \mbox{t}\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}size\ \mbox{ts}{\isacharparenright}
+\end{isabelle}%
+
+\end{quote}
+where \isa{set} returns the set of elements of a list---no special knowledge of sets is
+required in the following.
+First we have to understand why the recursive call of \isa{trev} underneath \isa{map} leads
+to the above condition. The reason is that \isacommand{recdef} ``knows'' that \isa{map} will
+apply \isa{trev} only to elements of \isa{\mbox{ts}}. Thus the above condition expresses that
+the size of the argument \isa{\mbox{t}\ {\isasymin}\ set\ \mbox{ts}} of any recursive call of \isa{trev} is strictly
+less than \isa{size\ {\isacharparenleft}App\ \mbox{f}\ \mbox{ts}{\isacharparenright}\ {\isacharequal}\ Suc\ {\isacharparenleft}term{\isacharunderscore}size\ \mbox{ts}{\isacharparenright}}.
+We will now prove the termination condition and continue with our definition.
+Below we return to the question of how \isacommand{recdef} ``knows'' about \isa{map}.%
+\end{isamarkuptext}%
+\end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:

--- a/doc-src/TutorialI/Recdef/document/Nested2.tex	Mon Aug 28 14:09:33 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested2.tex	Mon Aug 28 15:13:55 2000 +0200
@@ -4,8 +4,8 @@
 \noindent
 The termintion condition is easily proved by induction:%
 \end{isamarkuptext}%
-\isacommand{lemma}\ [simp]:\ {"}t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ <\ Suc(term\_size\ ts){"}\isanewline
-\isacommand{by}(induct\_tac\ ts,\ auto)%
+\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc{\isacharparenleft}term{\isacharunderscore}size\ ts{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ ts{\isacharcomma}\ auto{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
 By making this theorem a simplification rule, \isacommand{recdef}
@@ -15,30 +15,30 @@
 induction schema for type \isa{term} but the simpler one arising from
 \isa{trev}:%
 \end{isamarkuptext}%
-\isacommand{lemmas}\ [cong]\ =\ map\_cong\isanewline
-\isacommand{lemma}\ {"}trev(trev\ t)\ =\ t{"}\isanewline
-\isacommand{apply}(induct\_tac\ t\ rule:trev.induct)%
+\isacommand{lemmas}\ {\isacharbrackleft}cong{\isacharbrackright}\ {\isacharequal}\ map{\isacharunderscore}cong\isanewline
+\isacommand{lemma}\ {\isachardoublequote}trev{\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}\isanewline
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ rule{\isacharcolon}trev{\isachardot}induct{\isacharparenright}%
 \begin{isamarkuptxt}%
 \noindent
-This leaves us with a trivial base case \isa{trev\ (trev\ (Var\ \mbox{x}))\ =\ Var\ \mbox{x}} and the step case
+This leaves us with a trivial base case \isa{trev\ {\isacharparenleft}trev\ {\isacharparenleft}Var\ \mbox{x}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ Var\ \mbox{x}} and the step case
 \begin{quote}
 
 \begin{isabelle}%
-{\isasymforall}\mbox{t}.\ \mbox{t}\ {\isasymin}\ set\ \mbox{ts}\ {\isasymlongrightarrow}\ trev\ (trev\ \mbox{t})\ =\ \mbox{t}\ {\isasymLongrightarrow}\isanewline
-trev\ (trev\ (App\ \mbox{f}\ \mbox{ts}))\ =\ App\ \mbox{f}\ \mbox{ts}
+{\isasymforall}\mbox{t}{\isachardot}\ \mbox{t}\ {\isasymin}\ set\ \mbox{ts}\ {\isasymlongrightarrow}\ trev\ {\isacharparenleft}trev\ \mbox{t}{\isacharparenright}\ {\isacharequal}\ \mbox{t}\ {\isasymLongrightarrow}\isanewline
+trev\ {\isacharparenleft}trev\ {\isacharparenleft}App\ \mbox{f}\ \mbox{ts}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ App\ \mbox{f}\ \mbox{ts}
 \end{isabelle}%
 
 \end{quote}
 both of which are solved by simplification:%
 \end{isamarkuptxt}%
-\isacommand{by}(simp\_all\ del:map\_compose\ add:sym[OF\ map\_compose]\ rev\_map)%
+\isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ del{\isacharcolon}map{\isacharunderscore}compose\ add{\isacharcolon}sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}\ rev{\isacharunderscore}map{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
 If this surprises you, see Datatype/Nested2......
 
 The above definition of \isa{trev} is superior to the one in \S\ref{sec:nested-datatype}
 because it brings \isa{rev} into play, about which already know a lot, in particular
-\isa{rev\ (rev\ \mbox{xs})\ =\ \mbox{xs}}.
+\isa{rev\ {\isacharparenleft}rev\ \mbox{xs}{\isacharparenright}\ {\isacharequal}\ \mbox{xs}}.
 Thus this proof is a good example of an important principle:
 \begin{quote}
 \emph{Chose your definitions carefully\\
@@ -49,13 +49,13 @@
 conditions in the presence of higher-order functions like \isa{map}. For a start, if nothing
 were known about \isa{map}, \isa{map\ trev\ \mbox{ts}} might apply \isa{trev} to arbitrary terms,
 and thus \isacommand{recdef} would try to prove the unprovable
-\isa{size\ \mbox{t}\ <\ Suc\ (term\_size\ \mbox{ts})}, without any assumption about \isa{t}.
+\isa{size\ \mbox{t}\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}size\ \mbox{ts}{\isacharparenright}}, without any assumption about \isa{t}.
 Therefore \isacommand{recdef} has been supplied with the congruence theorem \isa{map\_cong}: 
 \begin{quote}
 
 \begin{isabelle}%
-{\isasymlbrakk}\mbox{xs}\ =\ \mbox{ys};\ {\isasymAnd}\mbox{x}.\ \mbox{x}\ {\isasymin}\ set\ \mbox{ys}\ {\isasymLongrightarrow}\ \mbox{f}\ \mbox{x}\ =\ \mbox{g}\ \mbox{x}{\isasymrbrakk}\isanewline
-{\isasymLongrightarrow}\ map\ \mbox{f}\ \mbox{xs}\ =\ map\ \mbox{g}\ \mbox{ys}
+{\isasymlbrakk}\mbox{xs}\ {\isacharequal}\ \mbox{ys}{\isacharsemicolon}\ {\isasymAnd}\mbox{x}{\isachardot}\ \mbox{x}\ {\isasymin}\ set\ \mbox{ys}\ {\isasymLongrightarrow}\ \mbox{f}\ \mbox{x}\ {\isacharequal}\ \mbox{g}\ \mbox{x}{\isasymrbrakk}\isanewline
+{\isasymLongrightarrow}\ map\ \mbox{f}\ \mbox{xs}\ {\isacharequal}\ map\ \mbox{g}\ \mbox{ys}
 \end{isabelle}%
 
 \end{quote}

--- a/doc-src/TutorialI/Trie/document/Trie.tex	Mon Aug 28 14:09:33 2000 +0200
+++ b/doc-src/TutorialI/Trie/document/Trie.tex	Mon Aug 28 15:13:55 2000 +0200
@@ -44,7 +44,7 @@
 distinguishes the two cases whether the search string is empty or not:%
 \end{isamarkuptext}%
 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}lookup\ {\isacharparenleft}Trie\ None\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ as\ {\isacharequal}\ None{\isachardoublequote}\isanewline
-\isacommand{by}{\isacharparenleft}case{\isacharunderscore}tac\ as{\isacharcomma}\ auto{\isacharparenright}%
+\isacommand{by}{\isacharparenleft}case{\isacharunderscore}tac\ as{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
 \begin{isamarkuptext}%
 Things begin to get interesting with the definition of an update function
 that adds a new (string,value) pair to a trie, overwriting the old value
@@ -117,8 +117,8 @@
 This proof may look surprisingly straightforward. However, note that this
 comes at a cost: the proof script is unreadable because the
 intermediate proof states are invisible, and we rely on the (possibly
-brittle) magic of \isa{auto} (after the induction) to split the remaining
-goals up in such a way that case distinction on \isa{bs} makes sense and
+brittle) magic of \isa{auto} (\isa{simp\_all} will not do---try it) to split the subgoals
+of the induction up in such a way that case distinction on \isa{bs} makes sense and
 solves the proof. Part~\ref{Isar} shows you how to write readable and stable
 proofs.%
 \end{isamarkuptext}%

--- a/doc-src/TutorialI/isabelle.sty	Mon Aug 28 14:09:33 2000 +0200
+++ b/doc-src/TutorialI/isabelle.sty	Mon Aug 28 15:13:55 2000 +0200
@@ -17,9 +17,9 @@
 \newdimen\isa@parindent\newdimen\isa@parskip
 
 \newenvironment{isabelle}{%
-\isa@parindent\parindent\parindent0pt%
+\trivlist\isa@parindent\parindent\parindent0pt%
 \isa@parskip\parskip\parskip0pt%
-\isastyle}{}
+\isastyle\item\relax}{\endtrivlist}
 
 \newcommand{\isa}[1]{\emph{\isastyleminor #1}}
 

--- a/doc-src/TutorialI/isabellesym.sty	Mon Aug 28 14:09:33 2000 +0200
+++ b/doc-src/TutorialI/isabellesym.sty	Mon Aug 28 15:13:55 2000 +0200
@@ -5,6 +5,7 @@
 %%
 
 \usepackage{latexsym}
+%\usepackage{amssymb}
 %\usepackage[latin1]{inputenc}
 
 \newcommand{\bigsqcap}{\overline{|\,\,|}}  %just a hack
@@ -15,8 +16,10 @@
 \newcommand{\isasymDelta}{$\Delta$}
 \newcommand{\isasymTheta}{$\Theta$}
 \newcommand{\isasymLambda}{$\Lambda$}
+\newcommand{\isasymXi}{$\Xi$}
 \newcommand{\isasymPi}{$\Pi$}
 \newcommand{\isasymSigma}{$\Sigma$}
+\newcommand{\isasymUpsilon}{$\Upsilon$}
 \newcommand{\isasymPhi}{$\Phi$}
 \newcommand{\isasymPsi}{$\Psi$}
 \newcommand{\isasymOmega}{$\Omega$}
@@ -28,15 +31,17 @@
 \newcommand{\isasymzeta}{$\zeta$}
 \newcommand{\isasymeta}{$\eta$}
 \newcommand{\isasymtheta}{$\vartheta$}
+\newcommand{\isasymiota}{$\iota$}
 \newcommand{\isasymkappa}{$\kappa$}
 \newcommand{\isasymlambda}{$\lambda$}
 \newcommand{\isasymmu}{$\mu$}
 \newcommand{\isasymnu}{$\nu$}
 \newcommand{\isasymxi}{$\xi$}
 \newcommand{\isasympi}{$\pi$}
-\newcommand{\isasymrho}{$\rho$}
+\newcommand{\isasymrho}{$\varrho$}
 \newcommand{\isasymsigma}{$\sigma$}
 \newcommand{\isasymtau}{$\tau$}
+\newcommand{\isasymupsilon}{$\upsilon$}
 \newcommand{\isasymphi}{$\varphi$}
 \newcommand{\isasymchi}{$\chi$}
 \newcommand{\isasympsi}{$\psi$}
@@ -86,7 +91,7 @@
 \newcommand{\isasymLeftarrow}{\emph{$\Leftarrow$}}
 \newcommand{\isasymMidarrow}{\emph{$=$}}%deprecated
 \newcommand{\isasymRightarrow}{\emph{$\Rightarrow$}}
-\newcommand{\isasymbow}{\emph{$\frown$}}
+\newcommand{\isasymfrown}{\emph{$\frown$}}
 \newcommand{\isasymmapsto}{\emph{$\mapsto$}}
 \newcommand{\isasymleadsto}{\emph{$\leadsto$}}
 \newcommand{\isasymup}{\emph{$\uparrow$}}
@@ -150,3 +155,86 @@
 \newcommand{\isasymlbrace}{\emph{$\mathopen{\lbrace\mkern-4.5mu\mid}$}}
 \newcommand{\isasymrbrace}{\emph{$\mathclose{\mid\mkern-4.5mu\rbrace}$}}
 \newcommand{\isasymtop}{\emph{$\top$}}
+
+\newcommand{\isasymcong}{\emph{$\cong$}}
+\newcommand{\isasymclubsuit}{\emph{$\clubsuit$}}
+\newcommand{\isasymdiamondsuit}{\emph{$\diamondsuit$}}
+\newcommand{\isasymheartsuit}{\emph{$\heartsuit$}}
+\newcommand{\isasymspadesuit}{\emph{$\spadesuit$}}
+\newcommand{\isasymleftrightarrow}{\emph{$\leftrightarrow$}}
+\newcommand{\isasymge}{\emph{$\ge$}}
+\newcommand{\isasympropto}{\emph{$\propto$}}
+\newcommand{\isasympartial}{\emph{$\partial$}}
+\newcommand{\isasymdots}{\emph{$\dots$}}
+\newcommand{\isasymaleph}{\emph{$\aleph$}}
+\newcommand{\isasymIm}{\emph{$\Im$}}
+\newcommand{\isasymRe}{\emph{$\Re$}}
+\newcommand{\isasymwp}{\emph{$\wp$}}
+\newcommand{\isasymemptyset}{\emph{$\emptyset$}}
+\newcommand{\isasymangle}{\emph{$\angle$}}
+\newcommand{\isasymnabla}{\emph{$\nabla$}}
+\newcommand{\isasymProd}{\emph{$\prod$}}
+\newcommand{\isasymLeftrightarrow}{\emph{$\Leftrightarrow$}}
+\newcommand{\isasymUparrow}{\emph{$\Uparrow$}}
+\newcommand{\isasymDownarrow}{\emph{$\Downarrow$}}
+\newcommand{\isasymlozenge}{\emph{$\lozenge$}}
+\newcommand{\isasymlangle}{\emph{$\langle$}}
+\newcommand{\isasymrangle}{\emph{$\rangle$}}
+\newcommand{\isasymSum}{\emph{$\sum$}}
+\newcommand{\isasymintegral}{\emph{$\int$}}
+\newcommand{\isasymdagger}{\emph{$\dagger$}}
+\newcommand{\isasymsharp}{\emph{$\sharp$}}
+\newcommand{\isasymstar}{\emph{$\star$}}
+\newcommand{\isasymtriangleright}{\emph{$\triangleright$}}
+\newcommand{\isasymlhd}{\emph{$\lhd$}}
+\newcommand{\isasymtriangle}{\emph{$\triangle$}}
+\newcommand{\isasymrhd}{\emph{$\rhd$}}
+\newcommand{\isasymunlhd}{\emph{$\unlhd$}}
+\newcommand{\isasymunrhd}{\emph{$\unrhd$}}
+\newcommand{\isasymtriangleleft}{\emph{$\triangleleft$}}
+\newcommand{\isasymnatural}{\emph{$\natural$}}
+\newcommand{\isasymflat}{\emph{$\flat$}}
+\newcommand{\isasymamalg}{\emph{$\amalg$}}
+\newcommand{\isasymmho}{\emph{$\mho$}}
+\newcommand{\isasymupdownarrow}{\emph{$\updownarrow$}}
+\newcommand{\isasymlongmapsto}{\emph{$\longmapsto$}}
+\newcommand{\isasymUpdownarrow}{\emph{$\Updownarrow$}}
+\newcommand{\isasymhookleftarrow}{\emph{$\hookleftarrow$}}
+\newcommand{\isasymhookrightarrow}{\emph{$\hookrightarrow$}}
+\newcommand{\isasymrightleftharpoons}{\emph{$\rightleftharpoons$}}
+\newcommand{\isasymleftharpoondown}{\emph{$\leftharpoondown$}}
+\newcommand{\isasymrightharpoondown}{\emph{$\rightharpoondown$}}
+\newcommand{\isasymleftharpoonup}{\emph{$\leftharpoonup$}}
+\newcommand{\isasymrightharpoonup}{\emph{$\rightharpoonup$}}
+\newcommand{\isasymasymp}{\emph{$\asymp$}}
+\newcommand{\isasymminusplus}{\emph{$\mp$}}
+\newcommand{\isasymbowtie}{\emph{$\bowtie$}}
+\newcommand{\isasymcdots}{\emph{$\cdots$}}
+\newcommand{\isasymodot}{\emph{$\odot$}}
+\newcommand{\isasymsupset}{\emph{$\supset$}}
+\newcommand{\isasymsupseteq}{\emph{$\supseteq$}}
+\newcommand{\isasymsqsupset}{\emph{$\sqsupset$}}
+\newcommand{\isasymsqsupseteq}{\emph{$\sqsupseteq$}}
+\newcommand{\isasymll}{\emph{$\ll$}}
+\newcommand{\isasymgg}{\emph{$\gg$}}
+\newcommand{\isasymuplus}{\emph{$\uplus$}}
+\newcommand{\isasymsmile}{\emph{$\smile$}}
+\newcommand{\isasymsucceq}{\emph{$\succeq$}}
+\newcommand{\isasymstileturn}{\emph{$\dashv$}}
+\newcommand{\isasymOr}{\emph{$\bigvee$}}
+\newcommand{\isasymbiguplus}{\emph{$\biguplus$}}
+\newcommand{\isasymddagger}{\emph{$\ddagger$}}
+\newcommand{\isasymJoin}{\emph{$\Join$}}
+\newcommand{\isasymbool}{\emph{$\mathrm{I}\mkern-3.8mu\mathrm{B}$}}
+\newcommand{\isasymcomplex}{\emph{$\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu$}}
+\newcommand{\isasymnat}{\emph{$\mathrm{I}\mkern-3.8mu\mathrm{N}$}}
+\newcommand{\isasymrat}{\emph{$\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu$}}
+\newcommand{\isasymreal}{\emph{$\mathrm{I}\mkern-3.8mu\mathrm{R}$}}
+\newcommand{\isasymint}{\emph{$\mathsf{Z}\mkern-7.5mu\mathsf{Z}$}}
+
+%requires amssymb
+\newcommand{\isasymlesssim}{\emph{$\lesssim$}}
+\newcommand{\isasymgreatersim}{\emph{$\gtrsim$}}
+\newcommand{\isasymlessapprox}{\emph{$\lessapprox$}}
+\newcommand{\isasymgreaterapprox}{\emph{$\gtrapprox$}}
+\newcommand{\isasymtriangleq}{\emph{$\triangleq$}}