updated;

--- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Mon Aug 21 19:03:58 2000 +0200
+++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Mon Aug 21 19:17:07 2000 +0200
@@ -10,10 +10,10 @@
 a fixed set of binary operations: instead the expression contains the
 appropriate function itself.%
 \end{isamarkuptext}%
-\isacommand{types}\ 'v\ binop\ =\ {"}'v\ {\isasymRightarrow}\ 'v\ {\isasymRightarrow}\ 'v{"}\isanewline
-\isacommand{datatype}\ ('a,'v)expr\ =\ Cex\ 'v\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Vex\ 'a\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Bex\ {"}'v\ binop{"}\ \ {"}('a,'v)expr{"}\ \ {"}('a,'v)expr{"}%
+\isacommand{types}\ {\isacharprime}v\ binop\ {\isacharequal}\ {\isachardoublequote}{\isacharprime}v\ {\isasymRightarrow}\ {\isacharprime}v\ {\isasymRightarrow}\ {\isacharprime}v{\isachardoublequote}\isanewline
+\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr\ {\isacharequal}\ Cex\ {\isacharprime}v\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Vex\ {\isacharprime}a\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Bex\ {\isachardoublequote}{\isacharprime}v\ binop{\isachardoublequote}\ \ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr{\isachardoublequote}\ \ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 The three constructors represent constants, variables and the application of
@@ -22,20 +22,20 @@
 The value of an expression w.r.t.\ an environment that maps variables to
 values is easily defined:%
 \end{isamarkuptext}%
-\isacommand{consts}\ value\ ::\ {"}('a,'v)expr\ {\isasymRightarrow}\ ('a\ {\isasymRightarrow}\ 'v)\ {\isasymRightarrow}\ 'v{"}\isanewline
+\isacommand{consts}\ value\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}v{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}v{\isachardoublequote}\isanewline
 \isacommand{primrec}\isanewline
-{"}value\ (Cex\ v)\ env\ =\ v{"}\isanewline
-{"}value\ (Vex\ a)\ env\ =\ env\ a{"}\isanewline
-{"}value\ (Bex\ f\ e1\ e2)\ env\ =\ f\ (value\ e1\ env)\ (value\ e2\ env){"}%
+{\isachardoublequote}value\ {\isacharparenleft}Cex\ v{\isacharparenright}\ env\ {\isacharequal}\ v{\isachardoublequote}\isanewline
+{\isachardoublequote}value\ {\isacharparenleft}Vex\ a{\isacharparenright}\ env\ {\isacharequal}\ env\ a{\isachardoublequote}\isanewline
+{\isachardoublequote}value\ {\isacharparenleft}Bex\ f\ e\isadigit{1}\ e\isadigit{2}{\isacharparenright}\ env\ {\isacharequal}\ f\ {\isacharparenleft}value\ e\isadigit{1}\ env{\isacharparenright}\ {\isacharparenleft}value\ e\isadigit{2}\ env{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 The stack machine has three instructions: load a constant value onto the
 stack, load the contents of a certain address onto the stack, and apply a
 binary operation to the two topmost elements of the stack, replacing them by
 the result. As for \isa{expr}, addresses and values are type parameters:%
 \end{isamarkuptext}%
-\isacommand{datatype}\ ('a,'v)\ instr\ =\ Const\ 'v\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Load\ 'a\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Apply\ {"}'v\ binop{"}%
+\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}\ instr\ {\isacharequal}\ Const\ {\isacharprime}v\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Load\ {\isacharprime}a\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Apply\ {\isachardoublequote}{\isacharprime}v\ binop{\isachardoublequote}%
 \begin{isamarkuptext}%
 The execution of the stack machine is modelled by a function
 \isa{exec} that takes a list of instructions, a store (modelled as a
@@ -44,13 +44,13 @@
 and returns the stack at the end of the execution---the store remains
 unchanged:%
 \end{isamarkuptext}%
-\isacommand{consts}\ exec\ ::\ {"}('a,'v)instr\ list\ {\isasymRightarrow}\ ('a{\isasymRightarrow}'v)\ {\isasymRightarrow}\ 'v\ list\ {\isasymRightarrow}\ 'v\ list{"}\isanewline
+\isacommand{consts}\ exec\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}instr\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isasymRightarrow}{\isacharprime}v{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}v\ list\ {\isasymRightarrow}\ {\isacharprime}v\ list{\isachardoublequote}\isanewline
 \isacommand{primrec}\isanewline
-{"}exec\ []\ s\ vs\ =\ vs{"}\isanewline
-{"}exec\ (i\#is)\ s\ vs\ =\ (case\ i\ of\isanewline
-\ \ \ \ Const\ v\ \ {\isasymRightarrow}\ exec\ is\ s\ (v\#vs)\isanewline
-\ \ |\ Load\ a\ \ \ {\isasymRightarrow}\ exec\ is\ s\ ((s\ a)\#vs)\isanewline
-\ \ |\ Apply\ f\ \ {\isasymRightarrow}\ exec\ is\ s\ ((f\ (hd\ vs)\ (hd(tl\ vs)))\#(tl(tl\ vs)))){"}%
+{\isachardoublequote}exec\ {\isacharbrackleft}{\isacharbrackright}\ s\ vs\ {\isacharequal}\ vs{\isachardoublequote}\isanewline
+{\isachardoublequote}exec\ {\isacharparenleft}i{\isacharhash}is{\isacharparenright}\ s\ vs\ {\isacharequal}\ {\isacharparenleft}case\ i\ of\isanewline
+\ \ \ \ Const\ v\ \ {\isasymRightarrow}\ exec\ is\ s\ {\isacharparenleft}v{\isacharhash}vs{\isacharparenright}\isanewline
+\ \ {\isacharbar}\ Load\ a\ \ \ {\isasymRightarrow}\ exec\ is\ s\ {\isacharparenleft}{\isacharparenleft}s\ a{\isacharparenright}{\isacharhash}vs{\isacharparenright}\isanewline
+\ \ {\isacharbar}\ Apply\ f\ \ {\isasymRightarrow}\ exec\ is\ s\ {\isacharparenleft}{\isacharparenleft}f\ {\isacharparenleft}hd\ vs{\isacharparenright}\ {\isacharparenleft}hd{\isacharparenleft}tl\ vs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharhash}{\isacharparenleft}tl{\isacharparenleft}tl\ vs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 Recall that \isa{hd} and \isa{tl}
@@ -64,29 +64,29 @@
 The compiler is a function from expressions to a list of instructions. Its
 definition is pretty much obvious:%
 \end{isamarkuptext}%
-\isacommand{consts}\ comp\ ::\ {"}('a,'v)expr\ {\isasymRightarrow}\ ('a,'v)instr\ list{"}\isanewline
+\isacommand{consts}\ comp\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}instr\ list{\isachardoublequote}\isanewline
 \isacommand{primrec}\isanewline
-{"}comp\ (Cex\ v)\ \ \ \ \ \ \ =\ [Const\ v]{"}\isanewline
-{"}comp\ (Vex\ a)\ \ \ \ \ \ \ =\ [Load\ a]{"}\isanewline
-{"}comp\ (Bex\ f\ e1\ e2)\ =\ (comp\ e2)\ @\ (comp\ e1)\ @\ [Apply\ f]{"}%
+{\isachardoublequote}comp\ {\isacharparenleft}Cex\ v{\isacharparenright}\ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}Const\ v{\isacharbrackright}{\isachardoublequote}\isanewline
+{\isachardoublequote}comp\ {\isacharparenleft}Vex\ a{\isacharparenright}\ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}Load\ a{\isacharbrackright}{\isachardoublequote}\isanewline
+{\isachardoublequote}comp\ {\isacharparenleft}Bex\ f\ e\isadigit{1}\ e\isadigit{2}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}comp\ e\isadigit{2}{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}comp\ e\isadigit{1}{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}Apply\ f{\isacharbrackright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 Now we have to prove the correctness of the compiler, i.e.\ that the
 execution of a compiled expression results in the value of the expression:%
 \end{isamarkuptext}%
-\isacommand{theorem}\ {"}exec\ (comp\ e)\ s\ []\ =\ [value\ e\ s]{"}%
+\isacommand{theorem}\ {\isachardoublequote}exec\ {\isacharparenleft}comp\ e{\isacharparenright}\ s\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}value\ e\ s{\isacharbrackright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 This theorem needs to be generalized to%
 \end{isamarkuptext}%
-\isacommand{theorem}\ {"}{\isasymforall}vs.\ exec\ (comp\ e)\ s\ vs\ =\ (value\ e\ s)\ \#\ vs{"}%
+\isacommand{theorem}\ {\isachardoublequote}{\isasymforall}vs{\isachardot}\ exec\ {\isacharparenleft}comp\ e{\isacharparenright}\ s\ vs\ {\isacharequal}\ {\isacharparenleft}value\ e\ s{\isacharparenright}\ {\isacharhash}\ vs{\isachardoublequote}%
 \begin{isamarkuptxt}%
 \noindent
 which is proved by induction on \isa{e} followed by simplification, once
 we have the following lemma about executing the concatenation of two
 instruction sequences:%
 \end{isamarkuptxt}%
-\isacommand{lemma}\ exec\_app[simp]:\isanewline
-\ \ {"}{\isasymforall}vs.\ exec\ (xs@ys)\ s\ vs\ =\ exec\ ys\ s\ (exec\ xs\ s\ vs){"}%
+\isacommand{lemma}\ exec{\isacharunderscore}app{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequote}{\isasymforall}vs{\isachardot}\ exec\ {\isacharparenleft}xs{\isacharat}ys{\isacharparenright}\ s\ vs\ {\isacharequal}\ exec\ ys\ s\ {\isacharparenleft}exec\ xs\ s\ vs{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptxt}%
 \noindent
 This requires induction on \isa{xs} and ordinary simplification for the
@@ -94,14 +94,14 @@
 that contains two \isa{case}-expressions over instructions. Thus we add
 automatic case splitting as well, which finishes the proof:%
 \end{isamarkuptxt}%
-\isacommand{by}(induct\_tac\ xs,\ simp,\ simp\ split:\ instr.split)%
+\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
 Note that because \isaindex{auto} performs simplification, it can
 also be modified in the same way \isa{simp} can. Thus the proof can be
 rewritten as%
 \end{isamarkuptext}%
-\isacommand{by}(induct\_tac\ xs,\ auto\ split:\ instr.split)%
+\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ auto\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
 Although this is more compact, it is less clear for the reader of the proof.

--- a/doc-src/TutorialI/Datatype/ROOT.ML	Mon Aug 21 19:03:58 2000 +0200
+++ b/doc-src/TutorialI/Datatype/ROOT.ML	Mon Aug 21 19:17:07 2000 +0200
@@ -1,4 +1,3 @@
 use_thy "ABexpr";
 use_thy "unfoldnested";
-use_thy "Nested2";
 use_thy "Fundata";

--- a/doc-src/TutorialI/Datatype/document/ABexpr.tex	Mon Aug 21 19:03:58 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex	Mon Aug 21 19:17:07 2000 +0200
@@ -13,14 +13,14 @@
 \end{itemize}
 In Isabelle this becomes%
 \end{isamarkuptext}%
-\isacommand{datatype}\ 'a\ aexp\ =\ IF\ \ \ {"}'a\ bexp{"}\ {"}'a\ aexp{"}\ {"}'a\ aexp{"}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Sum\ \ {"}'a\ aexp{"}\ {"}'a\ aexp{"}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Diff\ {"}'a\ aexp{"}\ {"}'a\ aexp{"}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Var\ 'a\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Num\ nat\isanewline
-\isakeyword{and}\ \ \ \ \ \ 'a\ bexp\ =\ Less\ {"}'a\ aexp{"}\ {"}'a\ aexp{"}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ And\ \ {"}'a\ bexp{"}\ {"}'a\ bexp{"}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Neg\ \ {"}'a\ bexp{"}%
+\isacommand{datatype}\ {\isacharprime}a\ aexp\ {\isacharequal}\ IF\ \ \ {\isachardoublequote}{\isacharprime}a\ bexp{\isachardoublequote}\ {\isachardoublequote}{\isacharprime}a\ aexp{\isachardoublequote}\ {\isachardoublequote}{\isacharprime}a\ aexp{\isachardoublequote}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Sum\ \ {\isachardoublequote}{\isacharprime}a\ aexp{\isachardoublequote}\ {\isachardoublequote}{\isacharprime}a\ aexp{\isachardoublequote}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Diff\ {\isachardoublequote}{\isacharprime}a\ aexp{\isachardoublequote}\ {\isachardoublequote}{\isacharprime}a\ aexp{\isachardoublequote}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Var\ {\isacharprime}a\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Num\ nat\isanewline
+\isakeyword{and}\ \ \ \ \ \ {\isacharprime}a\ bexp\ {\isacharequal}\ Less\ {\isachardoublequote}{\isacharprime}a\ aexp{\isachardoublequote}\ {\isachardoublequote}{\isacharprime}a\ aexp{\isachardoublequote}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ And\ \ {\isachardoublequote}{\isacharprime}a\ bexp{\isachardoublequote}\ {\isachardoublequote}{\isacharprime}a\ bexp{\isachardoublequote}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Neg\ \ {\isachardoublequote}{\isacharprime}a\ bexp{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 Type \isa{aexp} is similar to \isa{expr} in \S\ref{sec:ExprCompiler},
@@ -29,8 +29,8 @@
 expressions can be arithmetic comparisons, conjunctions and negations.
 The semantics is fixed via two evaluation functions%
 \end{isamarkuptext}%
-\isacommand{consts}\ \ evala\ ::\ {"}'a\ aexp\ {\isasymRightarrow}\ ('a\ {\isasymRightarrow}\ nat)\ {\isasymRightarrow}\ nat{"}\isanewline
-\ \ \ \ \ \ \ \ evalb\ ::\ {"}'a\ bexp\ {\isasymRightarrow}\ ('a\ {\isasymRightarrow}\ nat)\ {\isasymRightarrow}\ bool{"}%
+\isacommand{consts}\ \ evala\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ aexp\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
+\ \ \ \ \ \ \ \ evalb\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ bexp\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 that take an expression and an environment (a mapping from variables \isa{'a} to values
@@ -40,22 +40,22 @@
 section:%
 \end{isamarkuptext}%
 \isacommand{primrec}\isanewline
-\ \ {"}evala\ (IF\ b\ a1\ a2)\ env\ =\isanewline
-\ \ \ \ \ (if\ evalb\ b\ env\ then\ evala\ a1\ env\ else\ evala\ a2\ env){"}\isanewline
-\ \ {"}evala\ (Sum\ a1\ a2)\ env\ =\ evala\ a1\ env\ +\ evala\ a2\ env{"}\isanewline
-\ \ {"}evala\ (Diff\ a1\ a2)\ env\ =\ evala\ a1\ env\ -\ evala\ a2\ env{"}\isanewline
-\ \ {"}evala\ (Var\ v)\ env\ =\ env\ v{"}\isanewline
-\ \ {"}evala\ (Num\ n)\ env\ =\ n{"}\isanewline
+\ \ {\isachardoublequote}evala\ {\isacharparenleft}IF\ b\ a\isadigit{1}\ a\isadigit{2}{\isacharparenright}\ env\ {\isacharequal}\isanewline
+\ \ \ \ \ {\isacharparenleft}if\ evalb\ b\ env\ then\ evala\ a\isadigit{1}\ env\ else\ evala\ a\isadigit{2}\ env{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}evala\ {\isacharparenleft}Sum\ a\isadigit{1}\ a\isadigit{2}{\isacharparenright}\ env\ {\isacharequal}\ evala\ a\isadigit{1}\ env\ {\isacharplus}\ evala\ a\isadigit{2}\ env{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}evala\ {\isacharparenleft}Diff\ a\isadigit{1}\ a\isadigit{2}{\isacharparenright}\ env\ {\isacharequal}\ evala\ a\isadigit{1}\ env\ {\isacharminus}\ evala\ a\isadigit{2}\ env{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}evala\ {\isacharparenleft}Var\ v{\isacharparenright}\ env\ {\isacharequal}\ env\ v{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}evala\ {\isacharparenleft}Num\ n{\isacharparenright}\ env\ {\isacharequal}\ n{\isachardoublequote}\isanewline
 \isanewline
-\ \ {"}evalb\ (Less\ a1\ a2)\ env\ =\ (evala\ a1\ env\ <\ evala\ a2\ env){"}\isanewline
-\ \ {"}evalb\ (And\ b1\ b2)\ env\ =\ (evalb\ b1\ env\ {\isasymand}\ evalb\ b2\ env){"}\isanewline
-\ \ {"}evalb\ (Neg\ b)\ env\ =\ ({\isasymnot}\ evalb\ b\ env){"}%
+\ \ {\isachardoublequote}evalb\ {\isacharparenleft}Less\ a\isadigit{1}\ a\isadigit{2}{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}evala\ a\isadigit{1}\ env\ {\isacharless}\ evala\ a\isadigit{2}\ env{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}evalb\ {\isacharparenleft}And\ b\isadigit{1}\ b\isadigit{2}{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}evalb\ b\isadigit{1}\ env\ {\isasymand}\ evalb\ b\isadigit{2}\ env{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}evalb\ {\isacharparenleft}Neg\ b{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}{\isasymnot}\ evalb\ b\ env{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 In the same fashion we also define two functions that perform substitution:%
 \end{isamarkuptext}%
-\isacommand{consts}\ substa\ ::\ {"}('a\ {\isasymRightarrow}\ 'b\ aexp)\ {\isasymRightarrow}\ 'a\ aexp\ {\isasymRightarrow}\ 'b\ aexp{"}\isanewline
-\ \ \ \ \ \ \ substb\ ::\ {"}('a\ {\isasymRightarrow}\ 'b\ aexp)\ {\isasymRightarrow}\ 'a\ bexp\ {\isasymRightarrow}\ 'b\ bexp{"}%
+\isacommand{consts}\ substa\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ aexp{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ aexp\ {\isasymRightarrow}\ {\isacharprime}b\ aexp{\isachardoublequote}\isanewline
+\ \ \ \ \ \ \ substb\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ aexp{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ bexp\ {\isasymRightarrow}\ {\isacharprime}b\ bexp{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 The first argument is a function mapping variables to expressions, the
@@ -64,16 +64,16 @@
 to \isa{'b}. Note that there are only arithmetic and no boolean variables.%
 \end{isamarkuptext}%
 \isacommand{primrec}\isanewline
-\ \ {"}substa\ s\ (IF\ b\ a1\ a2)\ =\isanewline
-\ \ \ \ \ IF\ (substb\ s\ b)\ (substa\ s\ a1)\ (substa\ s\ a2){"}\isanewline
-\ \ {"}substa\ s\ (Sum\ a1\ a2)\ =\ Sum\ (substa\ s\ a1)\ (substa\ s\ a2){"}\isanewline
-\ \ {"}substa\ s\ (Diff\ a1\ a2)\ =\ Diff\ (substa\ s\ a1)\ (substa\ s\ a2){"}\isanewline
-\ \ {"}substa\ s\ (Var\ v)\ =\ s\ v{"}\isanewline
-\ \ {"}substa\ s\ (Num\ n)\ =\ Num\ n{"}\isanewline
+\ \ {\isachardoublequote}substa\ s\ {\isacharparenleft}IF\ b\ a\isadigit{1}\ a\isadigit{2}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ IF\ {\isacharparenleft}substb\ s\ b{\isacharparenright}\ {\isacharparenleft}substa\ s\ a\isadigit{1}{\isacharparenright}\ {\isacharparenleft}substa\ s\ a\isadigit{2}{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}substa\ s\ {\isacharparenleft}Sum\ a\isadigit{1}\ a\isadigit{2}{\isacharparenright}\ {\isacharequal}\ Sum\ {\isacharparenleft}substa\ s\ a\isadigit{1}{\isacharparenright}\ {\isacharparenleft}substa\ s\ a\isadigit{2}{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}substa\ s\ {\isacharparenleft}Diff\ a\isadigit{1}\ a\isadigit{2}{\isacharparenright}\ {\isacharequal}\ Diff\ {\isacharparenleft}substa\ s\ a\isadigit{1}{\isacharparenright}\ {\isacharparenleft}substa\ s\ a\isadigit{2}{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}substa\ s\ {\isacharparenleft}Var\ v{\isacharparenright}\ {\isacharequal}\ s\ v{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}substa\ s\ {\isacharparenleft}Num\ n{\isacharparenright}\ {\isacharequal}\ Num\ n{\isachardoublequote}\isanewline
 \isanewline
-\ \ {"}substb\ s\ (Less\ a1\ a2)\ =\ Less\ (substa\ s\ a1)\ (substa\ s\ a2){"}\isanewline
-\ \ {"}substb\ s\ (And\ b1\ b2)\ =\ And\ (substb\ s\ b1)\ (substb\ s\ b2){"}\isanewline
-\ \ {"}substb\ s\ (Neg\ b)\ =\ Neg\ (substb\ s\ b){"}%
+\ \ {\isachardoublequote}substb\ s\ {\isacharparenleft}Less\ a\isadigit{1}\ a\isadigit{2}{\isacharparenright}\ {\isacharequal}\ Less\ {\isacharparenleft}substa\ s\ a\isadigit{1}{\isacharparenright}\ {\isacharparenleft}substa\ s\ a\isadigit{2}{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}substb\ s\ {\isacharparenleft}And\ b\isadigit{1}\ b\isadigit{2}{\isacharparenright}\ {\isacharequal}\ And\ {\isacharparenleft}substb\ s\ b\isadigit{1}{\isacharparenright}\ {\isacharparenleft}substb\ s\ b\isadigit{2}{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}substb\ s\ {\isacharparenleft}Neg\ b{\isacharparenright}\ {\isacharequal}\ Neg\ {\isacharparenleft}substb\ s\ b{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 Now we can prove a fundamental theorem about the interaction between
 evaluation and substitution: applying a substitution $s$ to an expression $a$
@@ -84,9 +84,9 @@
 theorem in the induction step. Therefore you need to state and prove both
 theorems simultaneously:%
 \end{isamarkuptext}%
-\isacommand{lemma}\ {"}evala\ (substa\ s\ a)\ env\ =\ evala\ a\ ({\isasymlambda}x.\ evala\ (s\ x)\ env)\ {\isasymand}\isanewline
-\ \ \ \ \ \ \ \ evalb\ (substb\ s\ b)\ env\ =\ evalb\ b\ ({\isasymlambda}x.\ evala\ (s\ x)\ env){"}\isanewline
-\isacommand{apply}(induct\_tac\ a\ \isakeyword{and}\ b)%
+\isacommand{lemma}\ {\isachardoublequote}evala\ {\isacharparenleft}substa\ s\ a{\isacharparenright}\ env\ {\isacharequal}\ evala\ a\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ evala\ {\isacharparenleft}s\ x{\isacharparenright}\ env{\isacharparenright}\ {\isasymand}\isanewline
+\ \ \ \ \ \ \ \ evalb\ {\isacharparenleft}substb\ s\ b{\isacharparenright}\ env\ {\isacharequal}\ evalb\ b\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ evala\ {\isacharparenleft}s\ x{\isacharparenright}\ env{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ a\ \isakeyword{and}\ b{\isacharparenright}%
 \begin{isamarkuptxt}%
 \noindent
 The resulting 8 goals (one for each constructor) are proved in one fell swoop:%
@@ -102,7 +102,7 @@
 \end{ttbox}
 
 \begin{exercise}
-  Define a function \isa{norma} of type \isa{\mbox{'a}\ aexp\ {\isasymRightarrow}\ \mbox{'a}\ aexp} that
+  Define a function \isa{norma} of type \isa{\mbox{{\isacharprime}a}\ aexp\ {\isasymRightarrow}\ \mbox{{\isacharprime}a}\ aexp} that
   replaces \isa{IF}s with complex boolean conditions by nested
   \isa{IF}s where each condition is a \isa{Less} --- \isa{And} and
   \isa{Neg} should be eliminated completely. Prove that \isa{norma}

--- a/doc-src/TutorialI/Datatype/document/Fundata.tex	Mon Aug 21 19:03:58 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Fundata.tex	Mon Aug 21 19:17:07 2000 +0200
@@ -1,5 +1,5 @@
 \begin{isabelle}%
-\isacommand{datatype}\ ('a,'i)bigtree\ =\ Tip\ |\ Branch\ 'a\ {"}'i\ {\isasymRightarrow}\ ('a,'i)bigtree{"}%
+\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree\ {\isacharequal}\ Tip\ {\isacharbar}\ Branch\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}i\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent Parameter \isa{'a} is the type of values stored in
 the \isa{Branch}es of the tree, whereas \isa{'i} is the index
@@ -11,33 +11,33 @@
 \begin{quote}
 
 \begin{isabelle}%
-Branch\ 0\ ({\isasymlambda}\mbox{i}.\ Branch\ \mbox{i}\ ({\isasymlambda}\mbox{n}.\ Tip))
+Branch\ \isadigit{0}\ {\isacharparenleft}{\isasymlambda}\mbox{i}{\isachardot}\ Branch\ \mbox{i}\ {\isacharparenleft}{\isasymlambda}\mbox{n}{\isachardot}\ Tip{\isacharparenright}{\isacharparenright}
 \end{isabelle}%
 
 \end{quote}
-of type \isa{(nat,\ nat)\ bigtree} is the tree whose
+of type \isa{{\isacharparenleft}nat{\isacharcomma}\ nat{\isacharparenright}\ bigtree} is the tree whose
 root is labeled with 0 and whose $i$th subtree is labeled with $i$ and
 has merely \isa{Tip}s as further subtrees.
 
 Function \isa{map_bt} applies a function to all labels in a \isa{bigtree}:%
 \end{isamarkuptext}%
-\isacommand{consts}\ map\_bt\ ::\ {"}('a\ {\isasymRightarrow}\ 'b)\ {\isasymRightarrow}\ ('a,'i)bigtree\ {\isasymRightarrow}\ ('b,'i)bigtree{"}\isanewline
+\isacommand{consts}\ map{\isacharunderscore}bt\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree{\isachardoublequote}\isanewline
 \isacommand{primrec}\isanewline
-{"}map\_bt\ f\ Tip\ \ \ \ \ \ \ \ \ \ =\ Tip{"}\isanewline
-{"}map\_bt\ f\ (Branch\ a\ F)\ =\ Branch\ (f\ a)\ ({\isasymlambda}i.\ map\_bt\ f\ (F\ i)){"}%
+{\isachardoublequote}map{\isacharunderscore}bt\ f\ Tip\ \ \ \ \ \ \ \ \ \ {\isacharequal}\ Tip{\isachardoublequote}\isanewline
+{\isachardoublequote}map{\isacharunderscore}bt\ f\ {\isacharparenleft}Branch\ a\ F{\isacharparenright}\ {\isacharequal}\ Branch\ {\isacharparenleft}f\ a{\isacharparenright}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ map{\isacharunderscore}bt\ f\ {\isacharparenleft}F\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent This is a valid \isacommand{primrec} definition because the
 recursive calls of \isa{map_bt} involve only subtrees obtained from
 \isa{F}, i.e.\ the left-hand side. Thus termination is assured.  The
-seasoned functional programmer might have written \isa{map\_bt\ \mbox{f}\ {\isasymcirc}\ \mbox{F}}
-instead of \isa{{\isasymlambda}\mbox{i}.\ map\_bt\ \mbox{f}\ (\mbox{F}\ \mbox{i})}, but the former is not accepted by
+seasoned functional programmer might have written \isa{map{\isacharunderscore}bt\ \mbox{f}\ {\isasymcirc}\ \mbox{F}}
+instead of \isa{{\isasymlambda}\mbox{i}{\isachardot}\ map{\isacharunderscore}bt\ \mbox{f}\ {\isacharparenleft}\mbox{F}\ \mbox{i}{\isacharparenright}}, but the former is not accepted by
 Isabelle because the termination proof is not as obvious since
 \isa{map_bt} is only partially applied.
 
 The following lemma has a canonical proof%
 \end{isamarkuptext}%
-\isacommand{lemma}\ {"}map\_bt\ (g\ o\ f)\ T\ =\ map\_bt\ g\ (map\_bt\ f\ T){"}\isanewline
-\isacommand{by}(induct\_tac\ {"}T{"},\ auto)%
+\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}%
 \begin{isamarkuptext}%
 \noindent
 but it is worth taking a look at the proof state after the induction step

--- a/doc-src/TutorialI/Datatype/document/unfoldnested.tex	Mon Aug 21 19:03:58 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/unfoldnested.tex	Mon Aug 21 19:17:07 2000 +0200
@@ -1,6 +1,6 @@
 \begin{isabelle}%
-\isacommand{datatype}\ ('a,'b){"}term{"}\ =\ Var\ 'a\ |\ App\ 'b\ {"}('a,'b)term\_list{"}\isanewline
-\isakeyword{and}\ ('a,'b)term\_list\ =\ Nil\ |\ Cons\ {"}('a,'b)term{"}\ {"}('a,'b)term\_list{"}\end{isabelle}%
+\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{\isacharunderscore}list{\isachardoublequote}\isanewline
+\isakeyword{and}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list\ {\isacharequal}\ Nil\ {\isacharbar}\ Cons\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list{\isachardoublequote}\end{isabelle}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"

--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Mon Aug 21 19:03:58 2000 +0200
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Mon Aug 21 19:17:07 2000 +0200
@@ -7,15 +7,15 @@
 constants by negation and conjunction. The following datatype serves exactly
 that purpose:%
 \end{isamarkuptext}%
-\isacommand{datatype}\ boolex\ =\ Const\ bool\ |\ Var\ nat\ |\ Neg\ boolex\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ And\ boolex\ boolex%
+\isacommand{datatype}\ boolex\ {\isacharequal}\ Const\ bool\ {\isacharbar}\ Var\ nat\ {\isacharbar}\ Neg\ boolex\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ And\ boolex\ boolex%
 \begin{isamarkuptext}%
 \noindent
 The two constants are represented by \isa{Const\ True} and
 \isa{Const\ False}. Variables are represented by terms of the form
 \isa{Var\ \mbox{n}}, where \isa{\mbox{n}} is a natural number (type \isa{nat}).
 For example, the formula $P@0 \land \neg P@1$ is represented by the term
-\isa{And\ (Var\ 0)\ (Neg\ (Var\ 1))}.
+\isa{And\ {\isacharparenleft}Var\ \isadigit{0}{\isacharparenright}\ {\isacharparenleft}Neg\ {\isacharparenleft}Var\ \isadigit{1}{\isacharparenright}{\isacharparenright}}.
 
 \subsubsection{What is the value of a boolean expression?}
 
@@ -24,12 +24,12 @@
   environment} of type \isa{nat\ {\isasymRightarrow}\ bool}, which maps variables to
 their values:%
 \end{isamarkuptext}%
-\isacommand{consts}\ value\ ::\ {"}boolex\ {\isasymRightarrow}\ (nat\ {\isasymRightarrow}\ bool)\ {\isasymRightarrow}\ bool{"}\isanewline
+\isacommand{consts}\ value\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}boolex\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
 \isacommand{primrec}\isanewline
-{"}value\ (Const\ b)\ env\ =\ b{"}\isanewline
-{"}value\ (Var\ x)\ \ \ env\ =\ env\ x{"}\isanewline
-{"}value\ (Neg\ b)\ \ \ env\ =\ ({\isasymnot}\ value\ b\ env){"}\isanewline
-{"}value\ (And\ b\ c)\ env\ =\ (value\ b\ env\ {\isasymand}\ value\ c\ env){"}%
+{\isachardoublequote}value\ {\isacharparenleft}Const\ b{\isacharparenright}\ env\ {\isacharequal}\ b{\isachardoublequote}\isanewline
+{\isachardoublequote}value\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ env\ {\isacharequal}\ env\ x{\isachardoublequote}\isanewline
+{\isachardoublequote}value\ {\isacharparenleft}Neg\ b{\isacharparenright}\ \ \ env\ {\isacharequal}\ {\isacharparenleft}{\isasymnot}\ value\ b\ env{\isacharparenright}{\isachardoublequote}\isanewline
+{\isachardoublequote}value\ {\isacharparenleft}And\ b\ c{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}value\ b\ env\ {\isasymand}\ value\ c\ env{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 \subsubsection{If-expressions}
@@ -39,17 +39,17 @@
 from constants (\isa{CIF}), variables (\isa{VIF}) and conditionals
 (\isa{IF}):%
 \end{isamarkuptext}%
-\isacommand{datatype}\ ifex\ =\ CIF\ bool\ |\ VIF\ nat\ |\ IF\ ifex\ ifex\ ifex%
+\isacommand{datatype}\ ifex\ {\isacharequal}\ CIF\ bool\ {\isacharbar}\ VIF\ nat\ {\isacharbar}\ IF\ ifex\ ifex\ ifex%
 \begin{isamarkuptext}%
 \noindent
 The evaluation if If-expressions proceeds as for \isa{boolex}:%
 \end{isamarkuptext}%
-\isacommand{consts}\ valif\ ::\ {"}ifex\ {\isasymRightarrow}\ (nat\ {\isasymRightarrow}\ bool)\ {\isasymRightarrow}\ bool{"}\isanewline
+\isacommand{consts}\ valif\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
 \isacommand{primrec}\isanewline
-{"}valif\ (CIF\ b)\ \ \ \ env\ =\ b{"}\isanewline
-{"}valif\ (VIF\ x)\ \ \ \ env\ =\ env\ x{"}\isanewline
-{"}valif\ (IF\ b\ t\ e)\ env\ =\ (if\ valif\ b\ env\ then\ valif\ t\ env\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ valif\ e\ env){"}%
+{\isachardoublequote}valif\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ env\ {\isacharequal}\ b{\isachardoublequote}\isanewline
+{\isachardoublequote}valif\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ env\ {\isacharequal}\ env\ x{\isachardoublequote}\isanewline
+{\isachardoublequote}valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}if\ valif\ b\ env\ then\ valif\ t\ env\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ valif\ e\ env{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \subsubsection{Transformation into and of If-expressions}
 
@@ -57,24 +57,24 @@
 formulae, whereas \isa{ifex} is designed for efficiency. It is easy to
 translate from \isa{boolex} into \isa{ifex}:%
 \end{isamarkuptext}%
-\isacommand{consts}\ bool2if\ ::\ {"}boolex\ {\isasymRightarrow}\ ifex{"}\isanewline
+\isacommand{consts}\ bool\isadigit{2}if\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}boolex\ {\isasymRightarrow}\ ifex{\isachardoublequote}\isanewline
 \isacommand{primrec}\isanewline
-{"}bool2if\ (Const\ b)\ =\ CIF\ b{"}\isanewline
-{"}bool2if\ (Var\ x)\ \ \ =\ VIF\ x{"}\isanewline
-{"}bool2if\ (Neg\ b)\ \ \ =\ IF\ (bool2if\ b)\ (CIF\ False)\ (CIF\ True){"}\isanewline
-{"}bool2if\ (And\ b\ c)\ =\ IF\ (bool2if\ b)\ (bool2if\ c)\ (CIF\ False){"}%
+{\isachardoublequote}bool\isadigit{2}if\ {\isacharparenleft}Const\ b{\isacharparenright}\ {\isacharequal}\ CIF\ b{\isachardoublequote}\isanewline
+{\isachardoublequote}bool\isadigit{2}if\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ {\isacharequal}\ VIF\ x{\isachardoublequote}\isanewline
+{\isachardoublequote}bool\isadigit{2}if\ {\isacharparenleft}Neg\ b{\isacharparenright}\ \ \ {\isacharequal}\ IF\ {\isacharparenleft}bool\isadigit{2}if\ b{\isacharparenright}\ {\isacharparenleft}CIF\ False{\isacharparenright}\ {\isacharparenleft}CIF\ True{\isacharparenright}{\isachardoublequote}\isanewline
+{\isachardoublequote}bool\isadigit{2}if\ {\isacharparenleft}And\ b\ c{\isacharparenright}\ {\isacharequal}\ IF\ {\isacharparenleft}bool\isadigit{2}if\ b{\isacharparenright}\ {\isacharparenleft}bool\isadigit{2}if\ c{\isacharparenright}\ {\isacharparenleft}CIF\ False{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 At last, we have something we can verify: that \isa{bool2if} preserves the
 value of its argument:%
 \end{isamarkuptext}%
-\isacommand{lemma}\ {"}valif\ (bool2if\ b)\ env\ =\ value\ b\ env{"}%
+\isacommand{lemma}\ {\isachardoublequote}valif\ {\isacharparenleft}bool\isadigit{2}if\ b{\isacharparenright}\ env\ {\isacharequal}\ value\ b\ env{\isachardoublequote}%
 \begin{isamarkuptxt}%
 \noindent
 The proof is canonical:%
 \end{isamarkuptxt}%
-\isacommand{apply}(induct\_tac\ b)\isanewline
-\isacommand{by}(auto)%
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ b{\isacharparenright}\isanewline
+\isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
 In fact, all proofs in this case study look exactly like this. Hence we do
@@ -83,35 +83,35 @@
 More interesting is the transformation of If-expressions into a normal form
 where the first argument of \isa{IF} cannot be another \isa{IF} but
 must be a constant or variable. Such a normal form can be computed by
-repeatedly replacing a subterm of the form \isa{IF\ (IF\ \mbox{b}\ \mbox{x}\ \mbox{y})\ \mbox{z}\ \mbox{u}} by
-\isa{IF\ \mbox{b}\ (IF\ \mbox{x}\ \mbox{z}\ \mbox{u})\ (IF\ \mbox{y}\ \mbox{z}\ \mbox{u})}, which has the same value. The following
+repeatedly replacing a subterm of the form \isa{IF\ {\isacharparenleft}IF\ \mbox{b}\ \mbox{x}\ \mbox{y}{\isacharparenright}\ \mbox{z}\ \mbox{u}} by
+\isa{IF\ \mbox{b}\ {\isacharparenleft}IF\ \mbox{x}\ \mbox{z}\ \mbox{u}{\isacharparenright}\ {\isacharparenleft}IF\ \mbox{y}\ \mbox{z}\ \mbox{u}{\isacharparenright}}, which has the same value. The following
 primitive recursive functions perform this task:%
 \end{isamarkuptext}%
-\isacommand{consts}\ normif\ ::\ {"}ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex{"}\isanewline
+\isacommand{consts}\ normif\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex{\isachardoublequote}\isanewline
 \isacommand{primrec}\isanewline
-{"}normif\ (CIF\ b)\ \ \ \ t\ e\ =\ IF\ (CIF\ b)\ t\ e{"}\isanewline
-{"}normif\ (VIF\ x)\ \ \ \ t\ e\ =\ IF\ (VIF\ x)\ t\ e{"}\isanewline
-{"}normif\ (IF\ b\ t\ e)\ u\ f\ =\ normif\ b\ (normif\ t\ u\ f)\ (normif\ e\ u\ f){"}\isanewline
+{\isachardoublequote}normif\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ t\ e\ {\isacharequal}\ IF\ {\isacharparenleft}CIF\ b{\isacharparenright}\ t\ e{\isachardoublequote}\isanewline
+{\isachardoublequote}normif\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ t\ e\ {\isacharequal}\ IF\ {\isacharparenleft}VIF\ x{\isacharparenright}\ t\ e{\isachardoublequote}\isanewline
+{\isachardoublequote}normif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ u\ f\ {\isacharequal}\ normif\ b\ {\isacharparenleft}normif\ t\ u\ f{\isacharparenright}\ {\isacharparenleft}normif\ e\ u\ f{\isacharparenright}{\isachardoublequote}\isanewline
 \isanewline
-\isacommand{consts}\ norm\ ::\ {"}ifex\ {\isasymRightarrow}\ ifex{"}\isanewline
+\isacommand{consts}\ norm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ ifex{\isachardoublequote}\isanewline
 \isacommand{primrec}\isanewline
-{"}norm\ (CIF\ b)\ \ \ \ =\ CIF\ b{"}\isanewline
-{"}norm\ (VIF\ x)\ \ \ \ =\ VIF\ x{"}\isanewline
-{"}norm\ (IF\ b\ t\ e)\ =\ normif\ b\ (norm\ t)\ (norm\ e){"}%
+{\isachardoublequote}norm\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ {\isacharequal}\ CIF\ b{\isachardoublequote}\isanewline
+{\isachardoublequote}norm\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ {\isacharequal}\ VIF\ x{\isachardoublequote}\isanewline
+{\isachardoublequote}norm\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ normif\ b\ {\isacharparenleft}norm\ t{\isacharparenright}\ {\isacharparenleft}norm\ e{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 Their interplay is a bit tricky, and we leave it to the reader to develop an
 intuitive understanding. Fortunately, Isabelle can help us to verify that the
 transformation preserves the value of the expression:%
 \end{isamarkuptext}%
-\isacommand{theorem}\ {"}valif\ (norm\ b)\ env\ =\ valif\ b\ env{"}%
+\isacommand{theorem}\ {\isachardoublequote}valif\ {\isacharparenleft}norm\ b{\isacharparenright}\ env\ {\isacharequal}\ valif\ b\ env{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 The proof is canonical, provided we first show the following simplification
 lemma (which also helps to understand what \isa{normif} does):%
 \end{isamarkuptext}%
-\isacommand{lemma}\ [simp]:\isanewline
-\ \ {"}{\isasymforall}t\ e.\ valif\ (normif\ b\ t\ e)\ env\ =\ valif\ (IF\ b\ t\ e)\ env{"}%
+\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ valif\ {\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 Note that the lemma does not have a name, but is implicitly used in the proof
@@ -120,18 +120,18 @@
 But how can we be sure that \isa{norm} really produces a normal form in
 the above sense? We define a function that tests If-expressions for normality%
 \end{isamarkuptext}%
-\isacommand{consts}\ normal\ ::\ {"}ifex\ {\isasymRightarrow}\ bool{"}\isanewline
+\isacommand{consts}\ normal\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
 \isacommand{primrec}\isanewline
-{"}normal(CIF\ b)\ =\ True{"}\isanewline
-{"}normal(VIF\ x)\ =\ True{"}\isanewline
-{"}normal(IF\ b\ t\ e)\ =\ (normal\ t\ {\isasymand}\ normal\ e\ {\isasymand}\isanewline
-\ \ \ \ \ (case\ b\ of\ CIF\ b\ {\isasymRightarrow}\ True\ |\ VIF\ x\ {\isasymRightarrow}\ True\ |\ IF\ x\ y\ z\ {\isasymRightarrow}\ False)){"}%
+{\isachardoublequote}normal{\isacharparenleft}CIF\ b{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequote}\isanewline
+{\isachardoublequote}normal{\isacharparenleft}VIF\ x{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequote}\isanewline
+{\isachardoublequote}normal{\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e\ {\isasymand}\isanewline
+\ \ \ \ \ {\isacharparenleft}case\ b\ of\ CIF\ b\ {\isasymRightarrow}\ True\ {\isacharbar}\ VIF\ x\ {\isasymRightarrow}\ True\ {\isacharbar}\ IF\ x\ y\ z\ {\isasymRightarrow}\ False{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 and prove \isa{normal(norm b)}. Of course, this requires a lemma about
 normality of \isa{normif}:%
 \end{isamarkuptext}%
-\isacommand{lemma}[simp]:\ {"}{\isasymforall}t\ e.\ normal(normif\ b\ t\ e)\ =\ (normal\ t\ {\isasymand}\ normal\ e){"}\end{isabelle}%
+\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}\end{isabelle}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"

--- 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}

--- a/doc-src/TutorialI/Misc/document/Itrev.tex	Mon Aug 21 19:03:58 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex	Mon Aug 21 19:17:07 2000 +0200
@@ -7,10 +7,10 @@
 \isa{rev} reqires an extra argument where the result is accumulated
 gradually, using only \isa{\#}:%
 \end{isamarkuptext}%
-\isacommand{consts}\ itrev\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a\ list\ {\isasymRightarrow}\ 'a\ list{"}\isanewline
+\isacommand{consts}\ itrev\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
 \isacommand{primrec}\isanewline
-{"}itrev\ []\ \ \ \ \ ys\ =\ ys{"}\isanewline
-{"}itrev\ (x\#xs)\ ys\ =\ itrev\ xs\ (x\#ys){"}%
+{\isachardoublequote}itrev\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ ys\ {\isacharequal}\ ys{\isachardoublequote}\isanewline
+{\isachardoublequote}itrev\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ ys\ {\isacharequal}\ itrev\ xs\ {\isacharparenleft}x{\isacharhash}ys{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent The behaviour of \isa{itrev} is simple: it reverses
 its first argument by stacking its elements onto the second argument,
@@ -21,12 +21,12 @@
 Naturally, we would like to show that \isa{itrev} does indeed reverse
 its first argument provided the second one is empty:%
 \end{isamarkuptext}%
-\isacommand{lemma}\ {"}itrev\ xs\ []\ =\ rev\ xs{"}%
+\isacommand{lemma}\ {\isachardoublequote}itrev\ xs\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ xs{\isachardoublequote}%
 \begin{isamarkuptxt}%
 \noindent
 There is no choice as to the induction variable, and we immediately simplify:%
 \end{isamarkuptxt}%
-\isacommand{apply}(induct\_tac\ xs,\ auto)%
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ auto{\isacharparenright}%
 \begin{isamarkuptxt}%
 \noindent
 Unfortunately, this is not a complete success:
@@ -43,7 +43,7 @@
 Of course one cannot do this na\"{\i}vely: \isa{itrev xs ys = rev xs} is
 just not true---the correct generalization is%
 \end{isamarkuptxt}%
-\isacommand{lemma}\ {"}itrev\ xs\ ys\ =\ rev\ xs\ @\ ys{"}%
+\isacommand{lemma}\ {\isachardoublequote}itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}%
 \begin{isamarkuptxt}%
 \noindent
 If \isa{ys} is replaced by \isa{[]}, the right-hand side simplifies to
@@ -64,10 +64,10 @@
 The induction hypothesis is still too weak, but this time it takes no
 intuition to generalize: the problem is that \isa{ys} is fixed throughout
 the subgoal, but the induction hypothesis needs to be applied with
-\isa{\mbox{a}\ \#\ \mbox{ys}} instead of \isa{ys}. Hence we prove the theorem
+\isa{\mbox{a}\ {\isacharhash}\ \mbox{ys}} instead of \isa{ys}. Hence we prove the theorem
 for all \isa{ys} instead of a fixed one:%
 \end{isamarkuptxt}%
-\isacommand{lemma}\ {"}{\isasymforall}ys.\ itrev\ xs\ ys\ =\ rev\ xs\ @\ ys{"}%
+\isacommand{lemma}\ {\isachardoublequote}{\isasymforall}ys{\isachardot}\ itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}%
 \begin{isamarkuptxt}%
 \noindent
 This time induction on \isa{xs} followed by simplification succeeds. This

--- a/doc-src/TutorialI/Misc/document/Tree.tex	Mon Aug 21 19:03:58 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/Tree.tex	Mon Aug 21 19:17:07 2000 +0200
@@ -4,19 +4,19 @@
 \noindent
 Define the datatype of binary trees%
 \end{isamarkuptext}%
-\isacommand{datatype}\ 'a\ tree\ =\ Tip\ |\ Node\ {"}'a\ tree{"}\ 'a\ {"}'a\ tree{"}%
+\isacommand{datatype}\ {\isacharprime}a\ tree\ {\isacharequal}\ Tip\ {\isacharbar}\ Node\ {\isachardoublequote}{\isacharprime}a\ tree{\isachardoublequote}\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}a\ tree{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 and a function \isa{mirror} that mirrors a binary tree
 by swapping subtrees (recursively). Prove%
 \end{isamarkuptext}%
-\isacommand{lemma}\ mirror\_mirror:\ {"}mirror(mirror\ t)\ =\ t{"}%
+\isacommand{lemma}\ mirror{\isacharunderscore}mirror{\isacharcolon}\ {\isachardoublequote}mirror{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 Define a function \isa{flatten} that flattens a tree into a list
 by traversing it in infix order. Prove%
 \end{isamarkuptext}%
-\isacommand{lemma}\ {"}flatten(mirror\ t)\ =\ rev(flatten\ t){"}\end{isabelle}%
+\isacommand{lemma}\ {\isachardoublequote}flatten{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ rev{\isacharparenleft}flatten\ t{\isacharparenright}{\isachardoublequote}\end{isabelle}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"

--- a/doc-src/TutorialI/Misc/document/Tree2.tex	Mon Aug 21 19:03:58 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/Tree2.tex	Mon Aug 21 19:17:07 2000 +0200
@@ -7,11 +7,11 @@
 A linear time version of \isa{flatten} again reqires an extra
 argument, the accumulator:%
 \end{isamarkuptext}%
-\isacommand{consts}\ flatten2\ ::\ {"}'a\ tree\ =>\ 'a\ list\ =>\ 'a\ list{"}%
+\isacommand{consts}\ flatten\isadigit{2}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ tree\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent Define \isa{flatten2} and prove%
 \end{isamarkuptext}%
-\isacommand{lemma}\ {"}flatten2\ t\ []\ =\ flatten\ t{"}\end{isabelle}%
+\isacommand{lemma}\ {\isachardoublequote}flatten\isadigit{2}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequote}\end{isabelle}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"

--- a/doc-src/TutorialI/Misc/document/arith1.tex	Mon Aug 21 19:03:58 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/arith1.tex	Mon Aug 21 19:17:07 2000 +0200
@@ -1,5 +1,5 @@
 \begin{isabelle}%
-\isacommand{lemma}\ {"}{\isasymlbrakk}\ {\isasymnot}\ m\ <\ n;\ m\ <\ n+1\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ =\ n{"}\isanewline
+\isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}\isadigit{1}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isanewline
 \end{isabelle}%
 %%% Local Variables:
 %%% mode: latex

--- a/doc-src/TutorialI/Misc/document/arith2.tex	Mon Aug 21 19:03:58 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/arith2.tex	Mon Aug 21 19:17:07 2000 +0200
@@ -1,6 +1,6 @@
 \begin{isabelle}%
-\isacommand{lemma}\ {"}min\ i\ (max\ j\ (k*k))\ =\ max\ (min\ (k*k)\ i)\ (min\ i\ (j::nat)){"}\isanewline
-\isacommand{by}(arith)\isanewline
+\isacommand{lemma}\ {\isachardoublequote}min\ i\ {\isacharparenleft}max\ j\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ max\ {\isacharparenleft}min\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}\ i{\isacharparenright}\ {\isacharparenleft}min\ i\ {\isacharparenleft}j{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{by}{\isacharparenleft}arith{\isacharparenright}\isanewline
 \end{isabelle}%
 %%% Local Variables:
 %%% mode: latex

--- a/doc-src/TutorialI/Misc/document/arith3.tex	Mon Aug 21 19:03:58 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/arith3.tex	Mon Aug 21 19:17:07 2000 +0200
@@ -1,5 +1,5 @@
 \begin{isabelle}%
-\isacommand{lemma}\ {"}n*n\ =\ n\ {\isasymLongrightarrow}\ n=0\ {\isasymor}\ n=1{"}\isanewline
+\isacommand{lemma}\ {\isachardoublequote}n{\isacharasterisk}n\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ n{\isacharequal}\isadigit{0}\ {\isasymor}\ n{\isacharequal}\isadigit{1}{\isachardoublequote}\isanewline
 \end{isabelle}%
 %%% Local Variables:
 %%% mode: latex

--- a/doc-src/TutorialI/Misc/document/arith4.tex	Mon Aug 21 19:03:58 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/arith4.tex	Mon Aug 21 19:17:07 2000 +0200
@@ -1,5 +1,5 @@
 \begin{isabelle}%
-\isacommand{lemma}\ {"}{\isasymnot}\ m\ <\ n\ {\isasymand}\ m\ <\ n+1\ {\isasymLongrightarrow}\ m\ =\ n{"}\isanewline
+\isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ m\ {\isacharless}\ n\ {\isasymand}\ m\ {\isacharless}\ n{\isacharplus}\isadigit{1}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isanewline
 \end{isabelle}%
 %%% Local Variables:
 %%% mode: latex

--- a/doc-src/TutorialI/Misc/document/asm_simp.tex	Mon Aug 21 19:03:58 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/asm_simp.tex	Mon Aug 21 19:17:07 2000 +0200
@@ -4,27 +4,27 @@
 By default, assumptions are part of the simplification process: they are used
 as simplification rules and are simplified themselves. For example:%
 \end{isamarkuptext}%
-\isacommand{lemma}\ {"}{\isasymlbrakk}\ xs\ @\ zs\ =\ ys\ @\ xs;\ []\ @\ xs\ =\ []\ @\ []\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ ys\ =\ zs{"}\isanewline
+\isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ xs\ {\isacharat}\ zs\ {\isacharequal}\ ys\ {\isacharat}\ xs{\isacharsemicolon}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ ys\ {\isacharequal}\ zs{\isachardoublequote}\isanewline
 \isacommand{by}\ simp%
 \begin{isamarkuptext}%
 \noindent
-The second assumption simplifies to \isa{\mbox{xs}\ =\ []}, which in turn
-simplifies the first assumption to \isa{\mbox{zs}\ =\ \mbox{ys}}, thus reducing the
-conclusion to \isa{\mbox{ys}\ =\ \mbox{ys}} and hence to \isa{True}.
+The second assumption simplifies to \isa{\mbox{xs}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}, which in turn
+simplifies the first assumption to \isa{\mbox{zs}\ {\isacharequal}\ \mbox{ys}}, thus reducing the
+conclusion to \isa{\mbox{ys}\ {\isacharequal}\ \mbox{ys}} and hence to \isa{True}.
 
 In some cases this may be too much of a good thing and may lead to
 nontermination:%
 \end{isamarkuptext}%
-\isacommand{lemma}\ {"}{\isasymforall}x.\ f\ x\ =\ g\ (f\ (g\ x))\ {\isasymLongrightarrow}\ f\ []\ =\ f\ []\ @\ []{"}%
+\isacommand{lemma}\ {\isachardoublequote}{\isasymforall}x{\isachardot}\ f\ x\ {\isacharequal}\ g\ {\isacharparenleft}f\ {\isacharparenleft}g\ x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ f\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ f\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}%
 \begin{isamarkuptxt}%
 \noindent
 cannot be solved by an unmodified application of \isa{simp} because the
-simplification rule \isa{\mbox{f}\ \mbox{x}\ =\ \mbox{g}\ (\mbox{f}\ (\mbox{g}\ \mbox{x}))} extracted from the assumption
+simplification rule \isa{\mbox{f}\ \mbox{x}\ {\isacharequal}\ \mbox{g}\ {\isacharparenleft}\mbox{f}\ {\isacharparenleft}\mbox{g}\ \mbox{x}{\isacharparenright}{\isacharparenright}} extracted from the assumption
 does not terminate. Isabelle notices certain simple forms of
 nontermination but not this one. The problem can be circumvented by
 explicitly telling the simplifier to ignore the assumptions:%
 \end{isamarkuptxt}%
-\isacommand{by}(simp\ (no\_asm))%
+\isacommand{by}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
 There are three options that influence the treatment of assumptions:

--- a/doc-src/TutorialI/Misc/document/case_splits.tex	Mon Aug 21 19:03:58 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/case_splits.tex	Mon Aug 21 19:17:07 2000 +0200
@@ -4,7 +4,7 @@
 Goals containing \isaindex{if}-expressions are usually proved by case
 distinction on the condition of the \isa{if}. For example the goal%
 \end{isamarkuptext}%
-\isacommand{lemma}\ {"}{\isasymforall}xs.\ if\ xs\ =\ []\ then\ rev\ xs\ =\ []\ else\ rev\ xs\ {\isasymnoteq}\ []{"}%
+\isacommand{lemma}\ {\isachardoublequote}{\isasymforall}xs{\isachardot}\ if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ rev\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ else\ rev\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}%
 \begin{isamarkuptxt}%
 \noindent
 can be split into
@@ -13,7 +13,7 @@
 \end{isabellepar}%
 by a degenerate form of simplification%
 \end{isamarkuptxt}%
-\isacommand{apply}(simp\ only:\ split:\ split\_if)%
+\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
 where no simplification rules are included (\isa{only:} is followed by the
@@ -25,7 +25,7 @@
 
 This splitting idea generalizes from \isa{if} to \isaindex{case}:%
 \end{isamarkuptext}%
-\isacommand{lemma}\ {"}(case\ xs\ of\ []\ {\isasymRightarrow}\ zs\ |\ y\#ys\ {\isasymRightarrow}\ y\#(ys@zs))\ =\ xs@zs{"}%
+\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ zs\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ y{\isacharhash}{\isacharparenleft}ys{\isacharat}zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequote}%
 \begin{isamarkuptxt}%
 \noindent
 becomes
@@ -35,7 +35,7 @@
 \end{isabellepar}%
 by typing%
 \end{isamarkuptxt}%
-\isacommand{apply}(simp\ only:\ split:\ list.split)%
+\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
 In contrast to \isa{if}-expressions, the simplifier does not split
@@ -43,7 +43,7 @@
 in case of recursive datatypes. Again, if the \isa{only:} modifier is
 dropped, the above goal is solved,%
 \end{isamarkuptext}%
-\isacommand{by}(simp\ split:\ list.split)%
+\isacommand{by}{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent%
 which \isacommand{apply}\isa{(simp)} alone will not do.
@@ -52,18 +52,18 @@
 \isa{$t$.split} which can be declared to be a \bfindex{split rule} either
 locally as above, or by giving it the \isa{split} attribute globally:%
 \end{isamarkuptext}%
-\isacommand{lemmas}\ [split]\ =\ list.split%
+\isacommand{lemmas}\ {\isacharbrackleft}split{\isacharbrackright}\ {\isacharequal}\ list{\isachardot}split%
 \begin{isamarkuptext}%
 \noindent
 The \isa{split} attribute can be removed with the \isa{del} modifier,
 either locally%
 \end{isamarkuptext}%
-\isacommand{apply}(simp\ split\ del:\ split\_if)%
+\isacommand{apply}{\isacharparenleft}simp\ split\ del{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
 or globally:%
 \end{isamarkuptext}%
-\isacommand{lemmas}\ [split\ del]\ =\ list.split\isanewline
+\isacommand{lemmas}\ {\isacharbrackleft}split\ del{\isacharbrackright}\ {\isacharequal}\ list{\isachardot}split\isanewline
 \end{isabelle}%
 %%% Local Variables:
 %%% mode: latex

--- a/doc-src/TutorialI/Misc/document/cases.tex	Mon Aug 21 19:03:58 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/cases.tex	Mon Aug 21 19:17:07 2000 +0200
@@ -1,7 +1,7 @@
 \begin{isabelle}%
 \isanewline
-\isacommand{lemma}\ {"}(case\ xs\ of\ []\ {\isasymRightarrow}\ []\ |\ y\#ys\ {\isasymRightarrow}\ xs)\ =\ xs{"}\isanewline
-\isacommand{apply}(case\_tac\ xs)%
+\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
+\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ xs{\isacharparenright}%
 \begin{isamarkuptxt}%
 \noindent
 results in the proof state
@@ -11,7 +11,7 @@
 \end{isabellepar}%
 which is solved automatically:%
 \end{isamarkuptxt}%
-\isacommand{by}(auto)\isanewline
+\isacommand{by}{\isacharparenleft}auto{\isacharparenright}\isanewline
 \end{isabelle}%
 %%% Local Variables:
 %%% mode: latex

--- a/doc-src/TutorialI/Misc/document/cond_rewr.tex	Mon Aug 21 19:03:58 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/cond_rewr.tex	Mon Aug 21 19:17:07 2000 +0200
@@ -4,16 +4,16 @@
 So far all examples of rewrite rules were equations. The simplifier also
 accepts \emph{conditional} equations, for example%
 \end{isamarkuptext}%
-\isacommand{lemma}\ hd\_Cons\_tl[simp]:\ {"}xs\ {\isasymnoteq}\ []\ \ {\isasymLongrightarrow}\ \ hd\ xs\ \#\ tl\ xs\ =\ xs{"}\isanewline
-\isacommand{by}(case\_tac\ xs,\ simp,\ simp)%
+\isacommand{lemma}\ hd{\isacharunderscore}Cons{\isacharunderscore}tl{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ \ {\isasymLongrightarrow}\ \ hd\ xs\ {\isacharhash}\ tl\ xs\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
+\isacommand{by}{\isacharparenleft}case{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
 Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a
 sequence of methods. Assuming that the simplification rule
-\isa{(rev\ \mbox{xs}\ =\ [])\ =\ (\mbox{xs}\ =\ [])}
+\isa{{\isacharparenleft}rev\ \mbox{xs}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}\mbox{xs}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}}
 is present as well,%
 \end{isamarkuptext}%
-\isacommand{lemma}\ {"}xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd(rev\ xs)\ \#\ tl(rev\ xs)\ =\ rev\ xs{"}%
+\isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharhash}\ tl{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ rev\ xs{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 is proved by plain simplification:

--- a/doc-src/TutorialI/Misc/document/def_rewr.tex	Mon Aug 21 19:03:58 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/def_rewr.tex	Mon Aug 21 19:17:07 2000 +0200
@@ -9,19 +9,19 @@
 enough lemmas that characterize the concept sufficiently for us to forget the
 original definition. For example, given%
 \end{isamarkuptext}%
-\isacommand{constdefs}\ exor\ ::\ {"}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{"}\isanewline
-\ \ \ \ \ \ \ \ \ {"}exor\ A\ B\ {\isasymequiv}\ (A\ {\isasymand}\ {\isasymnot}B)\ {\isasymor}\ ({\isasymnot}A\ {\isasymand}\ B){"}%
+\isacommand{constdefs}\ exor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
+\ \ \ \ \ \ \ \ \ {\isachardoublequote}exor\ A\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 we may want to prove%
 \end{isamarkuptext}%
-\isacommand{lemma}\ {"}exor\ A\ ({\isasymnot}A){"}%
+\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}%
 \end{isamarkuptxt}%
-\isacommand{apply}(unfold\ exor\_def)%
+\isacommand{apply}{\isacharparenleft}unfold\ exor{\isacharunderscore}def{\isacharparenright}%
 \begin{isamarkuptxt}%
 \noindent
 It unfolds the given list of definitions (here merely one) in all subgoals:
@@ -33,7 +33,7 @@
 In case we want to expand a definition in the middle of a proof, we can
 simply include it locally:%
 \end{isamarkuptxt}%
-\isacommand{apply}(simp\ add:\ exor\_def)%
+\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ exor{\isacharunderscore}def{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
 In fact, this one command proves the above lemma directly.

--- a/doc-src/TutorialI/Misc/document/fakenat.tex	Mon Aug 21 19:03:58 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/fakenat.tex	Mon Aug 21 19:17:07 2000 +0200
@@ -5,7 +5,7 @@
 The type \isaindexbold{nat}\index{*0|bold}\index{*Suc|bold} of natural
 numbers is predefined and behaves like%
 \end{isamarkuptext}%
-\isacommand{datatype}\ nat\ =\ 0\ |\ Suc\ nat\end{isabelle}%
+\isacommand{datatype}\ nat\ {\isacharequal}\ \isadigit{0}\ {\isacharbar}\ Suc\ nat\end{isabelle}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"

--- a/doc-src/TutorialI/Misc/document/let_rewr.tex	Mon Aug 21 19:03:58 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/let_rewr.tex	Mon Aug 21 19:17:07 2000 +0200
@@ -1,11 +1,11 @@
 \begin{isabelle}%
-\isacommand{lemma}\ {"}(let\ xs\ =\ []\ in\ xs@ys@xs)\ =\ ys{"}\isanewline
-\isacommand{by}(simp\ add:\ Let\_def)%
+\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}let\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ in\ xs{\isacharat}ys{\isacharat}xs{\isacharparenright}\ {\isacharequal}\ ys{\isachardoublequote}\isanewline
+\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}%
 \begin{isamarkuptext}%
 If, in a particular context, there is no danger of a combinatorial explosion
 of nested \isa{let}s one could even add \isa{Let_def} permanently:%
 \end{isamarkuptext}%
-\isacommand{lemmas}\ [simp]\ =\ Let\_def\end{isabelle}%
+\isacommand{lemmas}\ {\isacharbrackleft}simp{\isacharbrackright}\ {\isacharequal}\ Let{\isacharunderscore}def\end{isabelle}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"

--- a/doc-src/TutorialI/Misc/document/natsum.tex	Mon Aug 21 19:03:58 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex	Mon Aug 21 19:17:07 2000 +0200
@@ -6,22 +6,22 @@
 \begin{quote}
 
 \begin{isabelle}%
-case\ \mbox{n}\ of\ 0\ {\isasymRightarrow}\ 0\ |\ Suc\ \mbox{m}\ {\isasymRightarrow}\ \mbox{m}
+case\ \mbox{n}\ of\ \isadigit{0}\ {\isasymRightarrow}\ \isadigit{0}\ {\isacharbar}\ Suc\ \mbox{m}\ {\isasymRightarrow}\ \mbox{m}
 \end{isabelle}%
 
 \end{quote}
 primitive recursion, for example%
 \end{isamarkuptext}%
-\isacommand{consts}\ sum\ ::\ {"}nat\ {\isasymRightarrow}\ nat{"}\isanewline
-\isacommand{primrec}\ {"}sum\ 0\ =\ 0{"}\isanewline
-\ \ \ \ \ \ \ \ {"}sum\ (Suc\ n)\ =\ Suc\ n\ +\ sum\ n{"}%
+\isacommand{consts}\ sum\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
+\isacommand{primrec}\ {\isachardoublequote}sum\ \isadigit{0}\ {\isacharequal}\ \isadigit{0}{\isachardoublequote}\isanewline
+\ \ \ \ \ \ \ \ {\isachardoublequote}sum\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ Suc\ n\ {\isacharplus}\ sum\ n{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 and induction, for example%
 \end{isamarkuptext}%
-\isacommand{lemma}\ {"}sum\ n\ +\ sum\ n\ =\ n*(Suc\ n){"}\isanewline
-\isacommand{apply}(induct\_tac\ n)\isanewline
-\isacommand{by}(auto)\isanewline
+\isacommand{lemma}\ {\isachardoublequote}sum\ n\ {\isacharplus}\ sum\ n\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}\isanewline
+\isacommand{by}{\isacharparenleft}auto{\isacharparenright}\isanewline
 \end{isabelle}%
 %%% Local Variables:
 %%% mode: latex

--- a/doc-src/TutorialI/Misc/document/pairs.tex	Mon Aug 21 19:03:58 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/pairs.tex	Mon Aug 21 19:17:07 2000 +0200
@@ -15,8 +15,8 @@
 In addition to explicit $\lambda$-abstractions, tuple patterns can be used in
 most variable binding constructs. Typical examples are
 \begin{quote}
-\isa{let\ (\mbox{x},\ \mbox{y})\ =\ \mbox{f}\ \mbox{z}\ in\ (\mbox{y},\ \mbox{x})}\\
-\isa{case\ \mbox{xs}\ of\ []\ {\isasymRightarrow}\ 0\ |\ (\mbox{x},\ \mbox{y})\ \#\ \mbox{zs}\ {\isasymRightarrow}\ \mbox{x}\ +\ \mbox{y}}
+\isa{let\ {\isacharparenleft}\mbox{x}{\isacharcomma}\ \mbox{y}{\isacharparenright}\ {\isacharequal}\ \mbox{f}\ \mbox{z}\ in\ {\isacharparenleft}\mbox{y}{\isacharcomma}\ \mbox{x}{\isacharparenright}}\\
+\isa{case\ \mbox{xs}\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ \isadigit{0}\ {\isacharbar}\ {\isacharparenleft}\mbox{x}{\isacharcomma}\ \mbox{y}{\isacharparenright}\ {\isacharhash}\ \mbox{zs}\ {\isasymRightarrow}\ \mbox{x}\ {\isacharplus}\ \mbox{y}}
 \end{quote}
 Further important examples are quantifiers and sets (see~\S\ref{quant-pats}).%
 \end{isamarkuptext}%

--- a/doc-src/TutorialI/Misc/document/prime_def.tex	Mon Aug 21 19:03:58 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/prime_def.tex	Mon Aug 21 19:17:07 2000 +0200
@@ -1,6 +1,6 @@
 \begin{isabelle}%
 \isanewline
-\ \ \ \ {"}prime(p)\ {\isasymequiv}\ 1\ <\ p\ {\isasymand}\ (m\ dvd\ p\ {\isasymlongrightarrow}\ (m=1\ {\isasymor}\ m=p)){"}%
+\ \ \ \ {\isachardoublequote}prime{\isacharparenleft}p{\isacharparenright}\ {\isasymequiv}\ \isadigit{1}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}m\ dvd\ p\ {\isasymlongrightarrow}\ {\isacharparenleft}m{\isacharequal}\isadigit{1}\ {\isasymor}\ m{\isacharequal}p{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent\small
 where \isa{dvd} means ``divides''.
@@ -8,7 +8,7 @@
 right-hand side, which would introduce an inconsistency (why?). What you
 should have written is%
 \end{isamarkuptext}%
-\ {"}prime(p)\ {\isasymequiv}\ 1\ <\ p\ {\isasymand}\ ({\isasymforall}m.\ m\ dvd\ p\ {\isasymlongrightarrow}\ (m=1\ {\isasymor}\ m=p)){"}\end{isabelle}%
+\ {\isachardoublequote}prime{\isacharparenleft}p{\isacharparenright}\ {\isasymequiv}\ \isadigit{1}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}{\isasymforall}m{\isachardot}\ m\ dvd\ p\ {\isasymlongrightarrow}\ {\isacharparenleft}m{\isacharequal}\isadigit{1}\ {\isasymor}\ m{\isacharequal}p{\isacharparenright}{\isacharparenright}{\isachardoublequote}\end{isabelle}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"

--- a/doc-src/TutorialI/Misc/document/trace_simp.tex	Mon Aug 21 19:03:58 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/trace_simp.tex	Mon Aug 21 19:17:07 2000 +0200
@@ -5,9 +5,9 @@
 \ttindexbold{trace_simp} \rmindex{flag} to get a better idea of what is going
 on:%
 \end{isamarkuptext}%
-\isacommand{ML}\ {"}set\ trace\_simp{"}\isanewline
-\isacommand{lemma}\ {"}rev\ [a]\ =\ []{"}\isanewline
-\isacommand{apply}(simp)%
+\isacommand{ML}\ {\isachardoublequote}set\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline
+\isacommand{lemma}\ {\isachardoublequote}rev\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
+\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}%
 \begin{isamarkuptxt}%
 \noindent
 produces the trace
@@ -35,7 +35,7 @@
 invocations of the simplifier are often nested (e.g.\ when solving conditions
 of rewrite rules). Thus it is advisable to reset it:%
 \end{isamarkuptxt}%
-\isacommand{ML}\ {"}reset\ trace\_simp{"}\isanewline
+\isacommand{ML}\ {\isachardoublequote}reset\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline
 \end{isabelle}%
 %%% Local Variables:
 %%% mode: latex

--- a/doc-src/TutorialI/Misc/document/types.tex	Mon Aug 21 19:03:58 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/types.tex	Mon Aug 21 19:17:07 2000 +0200
@@ -1,7 +1,7 @@
 \begin{isabelle}%
-\isacommand{types}\ number\ \ \ \ \ \ \ =\ nat\isanewline
-\ \ \ \ \ \ gate\ \ \ \ \ \ \ \ \ =\ {"}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{"}\isanewline
-\ \ \ \ \ \ ('a,'b)alist\ =\ {"}('a\ *\ 'b)list{"}%
+\isacommand{types}\ number\ \ \ \ \ \ \ {\isacharequal}\ nat\isanewline
+\ \ \ \ \ \ gate\ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
+\ \ \ \ \ \ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}alist\ {\isacharequal}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isacharasterisk}\ {\isacharprime}b{\isacharparenright}list{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent\indexbold{*types}%
 Internally all synonyms are fully expanded.  As a consequence Isabelle's
@@ -9,8 +9,8 @@
 readability of theories.  Synonyms can be used just like any other
 type:%
 \end{isamarkuptext}%
-\isacommand{consts}\ nand\ ::\ gate\isanewline
-\ \ \ \ \ \ \ exor\ ::\ gate%
+\isacommand{consts}\ nand\ {\isacharcolon}{\isacharcolon}\ gate\isanewline
+\ \ \ \ \ \ \ exor\ {\isacharcolon}{\isacharcolon}\ gate%
 \begin{isamarkuptext}%
 \subsection{Constant definitions}
 \label{sec:ConstDefinitions}
@@ -19,8 +19,8 @@
 The above constants \isa{nand} and \isa{exor} are non-recursive and can
 therefore be defined directly by%
 \end{isamarkuptext}%
-\isacommand{defs}\ nand\_def:\ {"}nand\ A\ B\ {\isasymequiv}\ {\isasymnot}(A\ {\isasymand}\ B){"}\isanewline
-\ \ \ \ \ exor\_def:\ {"}exor\ A\ B\ {\isasymequiv}\ A\ {\isasymand}\ {\isasymnot}B\ {\isasymor}\ {\isasymnot}A\ {\isasymand}\ B{"}%
+\isacommand{defs}\ nand{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}nand\ A\ B\ {\isasymequiv}\ {\isasymnot}{\isacharparenleft}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ \ \ \ exor{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}exor\ A\ B\ {\isasymequiv}\ A\ {\isasymand}\ {\isasymnot}B\ {\isasymor}\ {\isasymnot}A\ {\isasymand}\ B{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent%
 where \isacommand{defs}\indexbold{*defs} is a keyword and \isa{nand_def} and
@@ -29,10 +29,10 @@
 that must be used in constant definitions.
 Declarations and definitions can also be merged%
 \end{isamarkuptext}%
-\isacommand{constdefs}\ nor\ ::\ gate\isanewline
-\ \ \ \ \ \ \ \ \ {"}nor\ A\ B\ {\isasymequiv}\ {\isasymnot}(A\ {\isasymor}\ B){"}\isanewline
-\ \ \ \ \ \ \ \ \ \ exor2\ ::\ gate\isanewline
-\ \ \ \ \ \ \ \ \ {"}exor2\ A\ B\ {\isasymequiv}\ (A\ {\isasymor}\ B)\ {\isasymand}\ ({\isasymnot}A\ {\isasymor}\ {\isasymnot}B){"}%
+\isacommand{constdefs}\ nor\ {\isacharcolon}{\isacharcolon}\ gate\isanewline
+\ \ \ \ \ \ \ \ \ {\isachardoublequote}nor\ A\ B\ {\isasymequiv}\ {\isasymnot}{\isacharparenleft}A\ {\isasymor}\ B{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ \ \ \ \ \ \ \ \ exor\isadigit{2}\ {\isacharcolon}{\isacharcolon}\ gate\isanewline
+\ \ \ \ \ \ \ \ \ {\isachardoublequote}exor\isadigit{2}\ A\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymor}\ B{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymnot}A\ {\isasymor}\ {\isasymnot}B{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent\indexbold{*constdefs}%
 in which case the default name of each definition is \isa{$f$_def}, where

--- a/doc-src/TutorialI/fp.tex	Mon Aug 21 19:03:58 2000 +0200
+++ b/doc-src/TutorialI/fp.tex	Mon Aug 21 19:17:07 2000 +0200
@@ -862,4 +862,4 @@
 \label{sec:advanced-ind}
 \input{Misc/document/AdvancedInd.tex}
 
-\input{Datatype/document/Nested2.tex}
+%\input{Datatype/document/Nested2.tex}

--- a/doc-src/TutorialI/isabelle.sty	Mon Aug 21 19:03:58 2000 +0200
+++ b/doc-src/TutorialI/isabelle.sty	Mon Aug 21 19:17:07 2000 +0200
@@ -8,34 +8,64 @@
 
 % isabelle environments
 
-\newcommand{\isabellestyle}{\small\tt\slshape}
+\newcommand{\isastyle}{\small\tt\slshape}
+\newcommand{\isastyleminor}{\small\tt\slshape}
+\newcommand{\isastyletext}{\normalsize\rm}
+\newcommand{\isastyletxt}{\rm}
+\newcommand{\isastylecmt}{\rm}
 
 \newdimen\isa@parindent\newdimen\isa@parskip
+
 \newenvironment{isabelle}{%
 \isa@parindent\parindent\parindent0pt%
 \isa@parskip\parskip\parskip0pt%
-\isabellestyle}{}
+\isastyle}{}
 
-\newcommand{\isa}[1]{\emph{\isabellestyle #1}}
-
-\newenvironment{isabellequote}%
-{\begin{quote}\begin{isabelle}\noindent}{\end{isabelle}\end{quote}}
+\newcommand{\isa}[1]{\emph{\isastyleminor #1}}
 
 \newcommand{\isanewline}{\mbox{}\\\mbox{}}
+\newcommand{\isadigit}[1]{#1}
 
-\chardef\isabraceleft=`\{
-\chardef\isabraceright=`\}
-\chardef\isatilde=`\~
-\chardef\isacircum=`\^
-\chardef\isabackslash=`\\
+\chardef\isacharbang=`\!
+\chardef\isachardoublequote=`\"
+\chardef\isacharhash=`\#
+\chardef\isachardollar=`\$
+\chardef\isacharpercent=`\%
+\chardef\isacharampersand=`\&
+\chardef\isacharprime=`\'
+\chardef\isacharparenleft=`\(
+\chardef\isacharparenright=`\)
+\chardef\isacharasterisk=`\*
+\chardef\isacharplus=`\+
+\chardef\isacharcomma=`\,
+\chardef\isacharminus=`\-
+\chardef\isachardot=`\.
+\chardef\isacharslash=`\/
+\chardef\isacharcolon=`\:
+\chardef\isacharsemicolon=`\;
+\chardef\isacharless=`\<
+\chardef\isacharequal=`\=
+\chardef\isachargreater=`\>
+\chardef\isacharquery=`\?
+\chardef\isacharat=`\@
+\chardef\isacharbrackleft=`\[
+\chardef\isacharbackslash=`\\
+\chardef\isacharbrackright=`\]
+\chardef\isacharcircum=`\^
+\chardef\isacharunderscore=`\_
+\chardef\isacharbackquote=`\`
+\chardef\isacharbraceleft=`\{
+\chardef\isacharbar=`\|
+\chardef\isacharbraceright=`\}
+\chardef\isachartilde=`\~
 
 
 % keyword and section markup
 
-\newcommand{\isacommand}[1]{\emph{\bf #1}}
-\newcommand{\isakeyword}[1]{\emph{\bf #1}}
-\newcommand{\isabeginblock}{\isakeyword{\{}}
-\newcommand{\isaendblock}{\isakeyword{\}}}
+\newcommand{\isakeyword}[1]
+{\emph{\bf\def\isachardot{.}\def\isacharunderscore{-}%
+\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
+\newcommand{\isacommand}[1]{\isakeyword{#1}}
 
 \newcommand{\isamarkupheader}[1]{\section{#1}}
 \newcommand{\isamarkupchapter}[1]{\chapter{#1}}
@@ -47,6 +77,48 @@
 \newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
 
 \newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\par\medskip}{\par\smallskip}
-\newenvironment{isamarkuptext}{\normalsize\rm\begin{isapar}}{\end{isapar}}
-\newenvironment{isamarkuptxt}{\rm\begin{isapar}}{\end{isapar}}
-\newcommand{\isamarkupcmt}[1]{{\rm--- #1}}
+\newenvironment{isamarkuptext}{\isastyletext\begin{isapar}}{\end{isapar}}
+\newenvironment{isamarkuptxt}{\isastyletxt\begin{isapar}}{\end{isapar}}
+\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
+
+
+% alternative styles -- default is "tt"
+
+\newcommand{\isabellestyle}{}
+\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
+
+\newcommand{\isabellestyleit}{%
+\renewcommand{\isastyle}{\small\it}%
+\renewcommand{\isastyleminor}{\it}%
+%\renewcommand{\isadigit}[1]{\emph{$##1$}}
+\renewcommand{\isacharbang}{\emph{$!$}}%
+\renewcommand{\isachardoublequote}{}%
+\renewcommand{\isacharhash}{\emph{$\#$}}%
+\renewcommand{\isachardollar}{\emph{$\$$}}%
+\renewcommand{\isacharpercent}{\emph{$\%$}}%
+\renewcommand{\isacharampersand}{\emph{$\&$}}%
+\renewcommand{\isacharprime}{$\mskip2mu{'}\mskip-2mu$}%
+\renewcommand{\isacharparenleft}{\emph{$($}}%
+\renewcommand{\isacharparenright}{\emph{$)$}}%
+\renewcommand{\isacharasterisk}{\emph{$*$}}%
+\renewcommand{\isacharplus}{\emph{$+$}}%
+\renewcommand{\isacharcomma}{\emph{$\mathord,$}}%
+\renewcommand{\isacharminus}{\emph{$-$}}%
+\renewcommand{\isachardot}{\emph{$\mathord.$}}%
+\renewcommand{\isacharslash}{\emph{$/$}}%
+\renewcommand{\isacharcolon}{\emph{$\mathord:$}}%
+\renewcommand{\isacharsemicolon}{\emph{$\mathord;$}}%
+\renewcommand{\isacharless}{\emph{$<$}}%
+\renewcommand{\isacharequal}{\emph{$=$}}%
+\renewcommand{\isachargreater}{\emph{$>$}}%
+%\renewcommand{\isacharquery}{\emph{$\mathord?$}}%
+\renewcommand{\isacharat}{\emph{$@$}}%
+\renewcommand{\isacharbrackleft}{\emph{$[$}}%
+\renewcommand{\isacharbrackright}{\emph{$]$}}%
+\renewcommand{\isacharunderscore}{-}%
+\renewcommand{\isacharbraceleft}{\emph{$\{$}}%
+\renewcommand{\isacharbar}{\emph{$\mid$}}%
+\renewcommand{\isacharbraceright}{\emph{$\}$}}%
+}
+
+\newcommand{\isabellestylesl}{\isabellestyleit\renewcommand{\isastyle}{\small\slshape}}