# HG changeset patch
# User nipkow
# Date 956642950 -7200
# Node ID 026f37a86ea7dd655c0bc89f8ae1af0465459084
# Parent  bfab4d4b7516963a6ed56f79d2b330692e8ea0e1
*** empty log message ***

diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/CodeGen/CodeGen.thy
--- a/doc-src/TutorialI/CodeGen/CodeGen.thy	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/CodeGen/CodeGen.thy	Tue Apr 25 08:09:10 2000 +0200
@@ -18,18 +18,18 @@
                      | Bex "'v binop"  "('a,'v)expr"  "('a,'v)expr";
 
 text{*\noindent
-The three constructors represent constants, variables and the combination of
-two subexpressions with a binary operation.
+The three constructors represent constants, variables and the application of
+a binary operation to two subexpressions.
 
 The value of an expression w.r.t.\ an environment that maps variables to
 values is easily defined:
 *}
 
-consts value :: "('a \\<Rightarrow> 'v) \\<Rightarrow> ('a,'v)expr \\<Rightarrow> 'v";
+consts value :: "('a,'v)expr \\<Rightarrow> ('a \\<Rightarrow> 'v) \\<Rightarrow> 'v";
 primrec
-"value env (Cex v) = v"
-"value env (Vex a) = env a"
-"value env (Bex f e1 e2) = f (value env e1) (value env e2)";
+"value (Cex v) env = v"
+"value (Vex a) env = env a"
+"value (Bex f e1 e2) env = f (value e1 env) (value e2 env)";
 
 text{*
 The stack machine has three instructions: load a constant value onto the
@@ -43,20 +43,21 @@
                        | Apply "'v binop";
 
 text{*
-The execution of the stack machine is modelled by a function \isa{exec}
-that takes a store (modelled as a function from addresses to values, just
-like the environment for evaluating expressions), a stack (modelled as a
-list) of values, and a list of instructions, and returns the stack at the end
-of the execution---the store remains unchanged:
+The execution of the stack machine is modelled by a function
+\isa{exec} that takes a list of instructions, a store (modelled as a
+function from addresses to values, just like the environment for
+evaluating expressions), and a stack (modelled as a list) of values,
+and returns the stack at the end of the execution---the store remains
+unchanged:
 *}
 
-consts exec :: "('a\\<Rightarrow>'v) \\<Rightarrow> 'v list \\<Rightarrow> ('a,'v)instr list \\<Rightarrow> 'v list";
+consts exec :: "('a,'v)instr list \\<Rightarrow> ('a\\<Rightarrow>'v) \\<Rightarrow> 'v list \\<Rightarrow> 'v list";
 primrec
-"exec s vs [] = vs"
-"exec s vs (i#is) = (case i of
-    Const v  \\<Rightarrow> exec s (v#vs) is
-  | Load a   \\<Rightarrow> exec s ((s a)#vs) is
-  | Apply f  \\<Rightarrow> exec s ( (f (hd vs) (hd(tl vs)))#(tl(tl vs)) ) is)";
+"exec [] s vs = vs"
+"exec (i#is) s vs = (case i of
+    Const v  \\<Rightarrow> exec is s (v#vs)
+  | Load a   \\<Rightarrow> exec is s ((s a)#vs)
+  | Apply f  \\<Rightarrow> exec is s ((f (hd vs) (hd(tl vs)))#(tl(tl vs))))";
 
 text{*\noindent
 Recall that \isa{hd} and \isa{tl}
@@ -81,13 +82,13 @@
 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:
 *}
-theorem "exec s [] (comp e) = [value s e]";
+theorem "exec (comp e) s [] = [value e s]";
 (*<*)oops;(*>*)
 text{*\noindent
 This theorem needs to be generalized to
 *}
 
-theorem "\\<forall>vs. exec s vs (comp e) = (value s e) # vs";
+theorem "\\<forall>vs. exec (comp e) s vs = (value e s) # vs";
 
 txt{*\noindent
 which is proved by induction on \isa{e} followed by simplification, once
@@ -96,7 +97,7 @@
 *}
 (*<*)oops;(*>*)
 lemma exec_app[simp]:
-  "\\<forall>vs. exec s vs (xs@ys) = exec s (exec s vs xs) ys"; 
+  "\\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"; 
 
 txt{*\noindent
 This requires induction on \isa{xs} and ordinary simplification for the
@@ -113,20 +114,20 @@
 *}
 (*<*)
 lemmas [simp del] = exec_app;
-lemma [simp]: "\\<forall>vs. exec s vs (xs@ys) = exec s (exec s vs xs) ys"; 
+lemma [simp]: "\\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"; 
 (*>*)
 apply(induct_tac xs, auto split: instr.split).;
 
 text{*\noindent
 Although this is more compact, it is less clear for the reader of the proof.
 
-We could now go back and prove \isa{exec s [] (comp e) = [value s e]}
+We could now go back and prove \isa{exec (comp e) s [] = [value e s]}
 merely by simplification with the generalized version we just proved.
 However, this is unnecessary because the generalized version fully subsumes
 its instance.
 *}
 (*<*)
-theorem "\\<forall>vs. exec s vs (comp e) = (value s e) # vs";
+theorem "\\<forall>vs. exec (comp e) s vs = (value e s) # vs";
 apply(induct_tac e, auto).;
 end
 (*>*)
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/CodeGen/document/CodeGen.tex
--- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Tue Apr 25 08:09:10 2000 +0200
@@ -16,17 +16,17 @@
 ~~~~~~~~~~~~~~~~~~~~~|~Bex~{"}'v~binop{"}~~{"}('a,'v)expr{"}~~{"}('a,'v)expr{"}%
 \begin{isamarkuptext}%
 \noindent
-The three constructors represent constants, variables and the combination of
-two subexpressions with a binary operation.
+The three constructors represent constants, variables and the application of
+a binary operation to two subexpressions.
 
 The value of an expression w.r.t.\ an environment that maps variables to
 values is easily defined:%
 \end{isamarkuptext}%
-\isacommand{consts}~value~::~{"}('a~{\isasymRightarrow}~'v)~{\isasymRightarrow}~('a,'v)expr~{\isasymRightarrow}~'v{"}\isanewline
+\isacommand{consts}~value~::~{"}('a,'v)expr~{\isasymRightarrow}~('a~{\isasymRightarrow}~'v)~{\isasymRightarrow}~'v{"}\isanewline
 \isacommand{primrec}\isanewline
-{"}value~env~(Cex~v)~=~v{"}\isanewline
-{"}value~env~(Vex~a)~=~env~a{"}\isanewline
-{"}value~env~(Bex~f~e1~e2)~=~f~(value~env~e1)~(value~env~e2){"}%
+{"}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){"}%
 \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
@@ -37,19 +37,20 @@
 ~~~~~~~~~~~~~~~~~~~~~~~|~Load~'a\isanewline
 ~~~~~~~~~~~~~~~~~~~~~~~|~Apply~{"}'v~binop{"}%
 \begin{isamarkuptext}%
-The execution of the stack machine is modelled by a function \isa{exec}
-that takes a store (modelled as a function from addresses to values, just
-like the environment for evaluating expressions), a stack (modelled as a
-list) of values, and a list of instructions, and returns the stack at the end
-of the execution---the store remains unchanged:%
+The execution of the stack machine is modelled by a function
+\isa{exec} that takes a list of instructions, a store (modelled as a
+function from addresses to values, just like the environment for
+evaluating expressions), and a stack (modelled as a list) of values,
+and returns the stack at the end of the execution---the store remains
+unchanged:%
 \end{isamarkuptext}%
-\isacommand{consts}~exec~::~{"}('a{\isasymRightarrow}'v)~{\isasymRightarrow}~'v~list~{\isasymRightarrow}~('a,'v)instr~list~{\isasymRightarrow}~'v~list{"}\isanewline
+\isacommand{consts}~exec~::~{"}('a,'v)instr~list~{\isasymRightarrow}~('a{\isasymRightarrow}'v)~{\isasymRightarrow}~'v~list~{\isasymRightarrow}~'v~list{"}\isanewline
 \isacommand{primrec}\isanewline
-{"}exec~s~vs~[]~=~vs{"}\isanewline
-{"}exec~s~vs~(i\#is)~=~(case~i~of\isanewline
-~~~~Const~v~~{\isasymRightarrow}~exec~s~(v\#vs)~is\isanewline
-~~|~Load~a~~~{\isasymRightarrow}~exec~s~((s~a)\#vs)~is\isanewline
-~~|~Apply~f~~{\isasymRightarrow}~exec~s~(~(f~(hd~vs)~(hd(tl~vs)))\#(tl(tl~vs))~)~is){"}%
+{"}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)))){"}%
 \begin{isamarkuptext}%
 \noindent
 Recall that \isa{hd} and \isa{tl}
@@ -72,12 +73,12 @@
 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~s~[]~(comp~e)~=~[value~s~e]{"}%
+\isacommand{theorem}~{"}exec~(comp~e)~s~[]~=~[value~e~s]{"}%
 \begin{isamarkuptext}%
 \noindent
 This theorem needs to be generalized to%
 \end{isamarkuptext}%
-\isacommand{theorem}~{"}{\isasymforall}vs.~exec~s~vs~(comp~e)~=~(value~s~e)~\#~vs{"}%
+\isacommand{theorem}~{"}{\isasymforall}vs.~exec~(comp~e)~s~vs~=~(value~e~s)~\#~vs{"}%
 \begin{isamarkuptxt}%
 \noindent
 which is proved by induction on \isa{e} followed by simplification, once
@@ -85,7 +86,7 @@
 instruction sequences:%
 \end{isamarkuptxt}%
 \isacommand{lemma}~exec\_app[simp]:\isanewline
-~~{"}{\isasymforall}vs.~exec~s~vs~(xs@ys)~=~exec~s~(exec~s~vs~xs)~ys{"}%
+~~{"}{\isasymforall}vs.~exec~(xs@ys)~s~vs~=~exec~ys~s~(exec~xs~s~vs){"}%
 \begin{isamarkuptxt}%
 \noindent
 This requires induction on \isa{xs} and ordinary simplification for the
@@ -105,7 +106,7 @@
 \noindent
 Although this is more compact, it is less clear for the reader of the proof.
 
-We could now go back and prove \isa{exec s [] (comp e) = [value s e]}
+We could now go back and prove \isa{exec (comp e) s [] = [value e s]}
 merely by simplification with the generalized version we just proved.
 However, this is unnecessary because the generalized version fully subsumes
 its instance.%
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Datatype/ABexpr.thy
--- a/doc-src/TutorialI/Datatype/ABexpr.thy	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Datatype/ABexpr.thy	Tue Apr 25 08:09:10 2000 +0200
@@ -33,28 +33,28 @@
 The semantics is fixed via two evaluation functions
 *}
 
-consts  evala :: "('a \\<Rightarrow> nat) \\<Rightarrow> 'a aexp \\<Rightarrow> nat"
-        evalb :: "('a \\<Rightarrow> nat) \\<Rightarrow> 'a bexp \\<Rightarrow> bool";
+consts  evala :: "'a aexp \\<Rightarrow> ('a \\<Rightarrow> nat) \\<Rightarrow> nat"
+        evalb :: "'a bexp \\<Rightarrow> ('a \\<Rightarrow> nat) \\<Rightarrow> bool";
 
 text{*\noindent
-that take an environment (a mapping from variables \isa{'a} to values
-\isa{nat}) and an expression and return its arithmetic/boolean
+that take an expression and an environment (a mapping from variables \isa{'a} to values
+\isa{nat}) and return its arithmetic/boolean
 value. Since the datatypes are mutually recursive, so are functions that
 operate on them. Hence they need to be defined in a single \isacommand{primrec}
 section:
 *}
 
 primrec
-  "evala env (IF b a1 a2) =
-     (if evalb env b then evala env a1 else evala env a2)"
-  "evala env (Sum a1 a2) = evala env a1 + evala env a2"
-  "evala env (Diff a1 a2) = evala env a1 - evala env a2"
-  "evala env (Var v) = env v"
-  "evala env (Num n) = n"
+  "evala (IF b a1 a2) env =
+     (if evalb b env then evala a1 env else evala a2 env)"
+  "evala (Sum a1 a2) env = evala a1 env + evala a2 env"
+  "evala (Diff a1 a2) env = evala a1 env - evala a2 env"
+  "evala (Var v) env = env v"
+  "evala (Num n) env = n"
 
-  "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
-  "evalb env (And b1 b2) = (evalb env b1 \\<and> evalb env b2)"
-  "evalb env (Neg b) = (\\<not> evalb env b)"
+  "evalb (Less a1 a2) env = (evala a1 env < evala a2 env)"
+  "evalb (And b1 b2) env = (evalb b1 env \\<and> evalb b2 env)"
+  "evalb (Neg b) env = (\\<not> evalb b env)"
 
 text{*\noindent
 In the same fashion we also define two functions that perform substitution:
@@ -93,8 +93,8 @@
 theorems simultaneously:
 *}
 
-lemma "evala env (substa s a) = evala (\\<lambda>x. evala env (s x)) a \\<and>
-        evalb env (substb s b) = evalb (\\<lambda>x. evala env (s x)) b";
+lemma "evala (substa s a) env = evala a (\\<lambda>x. evala (s x) env) \\<and>
+        evalb (substb s b) env = evalb b (\\<lambda>x. evala (s x) env)";
 apply(induct_tac a and b);
 
 txt{*\noindent
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Datatype/Fundata.thy
--- a/doc-src/TutorialI/Datatype/Fundata.thy	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Datatype/Fundata.thy	Tue Apr 25 08:09:10 2000 +0200
@@ -14,7 +14,7 @@
 term "Branch 0 (\\<lambda>i. Branch i (\\<lambda>n. Tip))";
 
 text{*\noindent of type \isa{(nat,nat)bigtree} is the tree whose
-root is labeled with 0 and whose $n$th subtree is labeled with $n$ and
+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}:
@@ -35,7 +35,7 @@
 
 The following lemma has a canonical proof  *}
 
-lemma "map_bt g (map_bt f T) = map_bt (g o f) T";
+lemma "map_bt (g o f) T = map_bt g (map_bt f T)";
 apply(induct_tac "T", auto).
 
 text{*\noindent
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Datatype/document/ABexpr.tex
--- a/doc-src/TutorialI/Datatype/document/ABexpr.tex	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex	Tue Apr 25 08:09:10 2000 +0200
@@ -29,27 +29,27 @@
 expressions can be arithmetic comparisons, conjunctions and negations.
 The semantics is fixed via two evaluation functions%
 \end{isamarkuptext}%
-\isacommand{consts}~~evala~::~{"}('a~{\isasymRightarrow}~nat)~{\isasymRightarrow}~'a~aexp~{\isasymRightarrow}~nat{"}\isanewline
-~~~~~~~~evalb~::~{"}('a~{\isasymRightarrow}~nat)~{\isasymRightarrow}~'a~bexp~{\isasymRightarrow}~bool{"}%
+\isacommand{consts}~~evala~::~{"}'a~aexp~{\isasymRightarrow}~('a~{\isasymRightarrow}~nat)~{\isasymRightarrow}~nat{"}\isanewline
+~~~~~~~~evalb~::~{"}'a~bexp~{\isasymRightarrow}~('a~{\isasymRightarrow}~nat)~{\isasymRightarrow}~bool{"}%
 \begin{isamarkuptext}%
 \noindent
-that take an environment (a mapping from variables \isa{'a} to values
-\isa{nat}) and an expression and return its arithmetic/boolean
+that take an expression and an environment (a mapping from variables \isa{'a} to values
+\isa{nat}) and return its arithmetic/boolean
 value. Since the datatypes are mutually recursive, so are functions that
 operate on them. Hence they need to be defined in a single \isacommand{primrec}
 section:%
 \end{isamarkuptext}%
 \isacommand{primrec}\isanewline
-~~{"}evala~env~(IF~b~a1~a2)~=\isanewline
-~~~~~(if~evalb~env~b~then~evala~env~a1~else~evala~env~a2){"}\isanewline
-~~{"}evala~env~(Sum~a1~a2)~=~evala~env~a1~+~evala~env~a2{"}\isanewline
-~~{"}evala~env~(Diff~a1~a2)~=~evala~env~a1~-~evala~env~a2{"}\isanewline
-~~{"}evala~env~(Var~v)~=~env~v{"}\isanewline
-~~{"}evala~env~(Num~n)~=~n{"}\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
 \isanewline
-~~{"}evalb~env~(Less~a1~a2)~=~(evala~env~a1~<~evala~env~a2){"}\isanewline
-~~{"}evalb~env~(And~b1~b2)~=~(evalb~env~b1~{\isasymand}~evalb~env~b2){"}\isanewline
-~~{"}evalb~env~(Neg~b)~=~({\isasymnot}~evalb~env~b){"}%
+~~{"}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){"}%
 \begin{isamarkuptext}%
 \noindent
 In the same fashion we also define two functions that perform substitution:%
@@ -84,8 +84,8 @@
 theorem in the induction step. Therefore you need to state and prove both
 theorems simultaneously:%
 \end{isamarkuptext}%
-\isacommand{lemma}~{"}evala~env~(substa~s~a)~=~evala~({\isasymlambda}x.~evala~env~(s~x))~a~{\isasymand}\isanewline
-~~~~~~~~evalb~env~(substb~s~b)~=~evalb~({\isasymlambda}x.~evala~env~(s~x))~b{"}\isanewline
+\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)%
 \begin{isamarkuptxt}%
 \noindent
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Datatype/document/Fundata.tex
--- a/doc-src/TutorialI/Datatype/document/Fundata.tex	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Fundata.tex	Tue Apr 25 08:09:10 2000 +0200
@@ -12,7 +12,7 @@
 \isacommand{term}~{"}Branch~0~({\isasymlambda}i.~Branch~i~({\isasymlambda}n.~Tip)){"}%
 \begin{isamarkuptext}%
 \noindent of type \isa{(nat,nat)bigtree} is the tree whose
-root is labeled with 0 and whose $n$th subtree is labeled with $n$ and
+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}:%
@@ -32,7 +32,7 @@
 
 The following lemma has a canonical proof%
 \end{isamarkuptext}%
-\isacommand{lemma}~{"}map\_bt~g~(map\_bt~f~T)~=~map\_bt~(g~o~f)~T{"}\isanewline
+\isacommand{lemma}~{"}map\_bt~(g~o~f)~T~=~map\_bt~g~(map\_bt~f~T){"}\isanewline
 \isacommand{apply}(induct\_tac~{"}T{"},~auto)\isacommand{.}%
 \begin{isamarkuptext}%
 \noindent
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Ifexpr/Ifexpr.thy
--- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Tue Apr 25 08:09:10 2000 +0200
@@ -61,7 +61,7 @@
 \subsubsection{Transformation into and of If-expressions}
 
 The type \isa{boolex} is close to the customary representation of logical
-formulae, whereas \isa{ifex} is designed for efficiency. Thus we need to
+formulae, whereas \isa{ifex} is designed for efficiency. It is easy to
 translate from \isa{boolex} into \isa{ifex}:
 *}
 
@@ -153,7 +153,8 @@
 normality of \isa{normif}:
 *}
 
-lemma [simp]: "\\<forall>t e. normal(normif b t e) = (normal t \\<and> normal e)";(*<*)
+lemma [simp]: "\\<forall>t e. normal(normif b t e) = (normal t \\<and> normal e)";
+(*<*)
 apply(induct_tac b);
 apply(auto).;
 
@@ -161,4 +162,5 @@
 apply(induct_tac b);
 apply(auto).;
 
-end(*>*)
+end
+(*>*)
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Ifexpr/document/Ifexpr.tex
--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Tue Apr 25 08:09:10 2000 +0200
@@ -54,7 +54,7 @@
 \subsubsection{Transformation into and of If-expressions}
 
 The type \isa{boolex} is close to the customary representation of logical
-formulae, whereas \isa{ifex} is designed for efficiency. Thus we need to
+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
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Misc/case_splits.thy
--- a/doc-src/TutorialI/Misc/case_splits.thy	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Misc/case_splits.thy	Tue Apr 25 08:09:10 2000 +0200
@@ -48,15 +48,16 @@
 In contrast to \isa{if}-expressions, the simplifier does not split
 \isa{case}-expressions by default because this can lead to nontermination
 in case of recursive datatypes. Again, if the \isa{only:} modifier is
-dropped, the above goal is solved, which \isacommand{apply}\isa{(simp)}
-alone will not do:
+dropped, the above goal is solved,
 *}
 (*<*)
 lemma "(case xs of [] \\<Rightarrow> zs | y#ys \\<Rightarrow> y#(ys@zs)) = xs@zs";
 (*>*)
 apply(simp split: list.split).;
 
-text{*
+text{*\noindent%
+which \isacommand{apply}\isa{(simp)} alone will not do.
+
 In general, every datatype $t$ comes with a theorem
 \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:
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Misc/cases.thy
--- a/doc-src/TutorialI/Misc/cases.thy	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Misc/cases.thy	Tue Apr 25 08:09:10 2000 +0200
@@ -5,11 +5,13 @@
 lemma "(case xs of [] \\<Rightarrow> [] | y#ys \\<Rightarrow> xs) = xs";
 apply(case_tac xs);
 
-txt{*
+txt{*\noindent
+results in the proof state
 \begin{isabellepar}%
 ~1.~xs~=~[]~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y~\#~ys~{\isasymRightarrow}~xs)~=~xs\isanewline
 ~2.~{\isasymAnd}a~list.~xs=a\#list~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y\#ys~{\isasymRightarrow}~xs)~=~xs%
 \end{isabellepar}%
+which is solved automatically:
 *}
 
 apply(auto).;
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Misc/cond_rewr.thy
--- a/doc-src/TutorialI/Misc/cond_rewr.thy	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Misc/cond_rewr.thy	Tue Apr 25 08:09:10 2000 +0200
@@ -23,7 +23,7 @@
 apply(simp).
 (*>*)
 text{*\noindent
-is proved by simplification:
+is proved by plain simplification:
 the conditional equation \isa{hd_Cons_tl} above
 can simplify \isa{hd(rev~xs)~\#~tl(rev~xs)} to \isa{rev xs}
 because the corresponding precondition \isa{rev xs \isasymnoteq\ []}
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Misc/document/case_splits.tex
--- a/doc-src/TutorialI/Misc/document/case_splits.tex	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/case_splits.tex	Tue Apr 25 08:09:10 2000 +0200
@@ -41,11 +41,13 @@
 In contrast to \isa{if}-expressions, the simplifier does not split
 \isa{case}-expressions by default because this can lead to nontermination
 in case of recursive datatypes. Again, if the \isa{only:} modifier is
-dropped, the above goal is solved, which \isacommand{apply}\isa{(simp)}
-alone will not do:%
+dropped, the above goal is solved,%
 \end{isamarkuptext}%
 \isacommand{apply}(simp~split:~list.split)\isacommand{.}%
 \begin{isamarkuptext}%
+\noindent%
+which \isacommand{apply}\isa{(simp)} alone will not do.
+
 In general, every datatype $t$ comes with a theorem
 \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:%
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Misc/document/cases.tex
--- a/doc-src/TutorialI/Misc/document/cases.tex	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/cases.tex	Tue Apr 25 08:09:10 2000 +0200
@@ -3,10 +3,13 @@
 \isacommand{lemma}~{"}(case~xs~of~[]~{\isasymRightarrow}~[]~|~y\#ys~{\isasymRightarrow}~xs)~=~xs{"}\isanewline
 \isacommand{apply}(case\_tac~xs)%
 \begin{isamarkuptxt}%
+\noindent
+results in the proof state
 \begin{isabellepar}%
 ~1.~xs~=~[]~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y~\#~ys~{\isasymRightarrow}~xs)~=~xs\isanewline
 ~2.~{\isasymAnd}a~list.~xs=a\#list~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y\#ys~{\isasymRightarrow}~xs)~=~xs%
-\end{isabellepar}%%
+\end{isabellepar}%
+which is solved automatically:%
 \end{isamarkuptxt}%
 \isacommand{apply}(auto)\isacommand{.}\isanewline
 \end{isabelle}%
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Misc/document/cond_rewr.tex
--- a/doc-src/TutorialI/Misc/document/cond_rewr.tex	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/cond_rewr.tex	Tue Apr 25 08:09:10 2000 +0200
@@ -19,7 +19,7 @@
 \isacommand{lemma}~{"}xs~{\isasymnoteq}~[]~{\isasymLongrightarrow}~hd(rev~xs)~\#~tl(rev~xs)~=~rev~xs{"}%
 \begin{isamarkuptext}%
 \noindent
-is proved by simplification:
+is proved by plain simplification:
 the conditional equation \isa{hd_Cons_tl} above
 can simplify \isa{hd(rev~xs)~\#~tl(rev~xs)} to \isa{rev xs}
 because the corresponding precondition \isa{rev xs \isasymnoteq\ []}
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Misc/document/let_rewr.tex
--- a/doc-src/TutorialI/Misc/document/let_rewr.tex	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/let_rewr.tex	Tue Apr 25 08:09:10 2000 +0200
@@ -3,6 +3,6 @@
 \isacommand{apply}(simp~add:~Let\_def)\isacommand{.}%
 \begin{isamarkuptext}%
 If, in a particular context, there is no danger of a combinatorial explosion
-of nested \texttt{let}s one could even add \texttt{Let_def} permanently:%
+of nested \isa{let}s one could even add \isa{Let_def} permanently:%
 \end{isamarkuptext}%
 \isacommand{theorems}~[simp]~=~Let\_def\end{isabelle}%
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Misc/document/trace_simp.tex
--- a/doc-src/TutorialI/Misc/document/trace_simp.tex	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/trace_simp.tex	Tue Apr 25 08:09:10 2000 +0200
@@ -31,7 +31,7 @@
 [x] = [] == False
 \end{ttbox}
 
-In more complicated cases, the trace can quite lenghty, especially since
+In more complicated cases, the trace can be quite lenghty, especially since
 invocations of the simplifier are often nested (e.g.\ when solving conditions
 of rewrite rules). Thus it is advisable to reset it:%
 \end{isamarkuptxt}%
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Misc/document/types.tex
--- a/doc-src/TutorialI/Misc/document/types.tex	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/types.tex	Tue Apr 25 08:09:10 2000 +0200
@@ -6,7 +6,7 @@
 \noindent\indexbold{*types}%
 Internally all synonyms are fully expanded.  As a consequence Isabelle's
 output never contains synonyms.  Their main purpose is to improve the
-readability of theory definitions.  Synonyms can be used just like any other
+readability of theories.  Synonyms can be used just like any other
 type:%
 \end{isamarkuptext}%
 \isacommand{consts}~nand~::~gate\isanewline
@@ -24,7 +24,7 @@
 \begin{isamarkuptext}%
 \noindent%
 where \isacommand{defs}\indexbold{*defs} is a keyword and \isa{nand_def} and
-\isa{exor_def} are arbitrary user-supplied names.
+\isa{exor_def} are user-supplied names.
 The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
 that should only be used in constant definitions.
 Declarations and definitions can also be merged%
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Misc/let_rewr.thy
--- a/doc-src/TutorialI/Misc/let_rewr.thy	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Misc/let_rewr.thy	Tue Apr 25 08:09:10 2000 +0200
@@ -6,7 +6,7 @@
 
 text{*
 If, in a particular context, there is no danger of a combinatorial explosion
-of nested \texttt{let}s one could even add \texttt{Let_def} permanently:
+of nested \isa{let}s one could even add \isa{Let_def} permanently:
 *}
 theorems [simp] = Let_def;
 (*<*)
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Misc/trace_simp.thy
--- a/doc-src/TutorialI/Misc/trace_simp.thy	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Misc/trace_simp.thy	Tue Apr 25 08:09:10 2000 +0200
@@ -33,7 +33,7 @@
 [x] = [] == False
 \end{ttbox}
 
-In more complicated cases, the trace can quite lenghty, especially since
+In more complicated cases, the trace can be quite lenghty, especially since
 invocations of the simplifier are often nested (e.g.\ when solving conditions
 of rewrite rules). Thus it is advisable to reset it:
 *}
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Misc/types.thy
--- a/doc-src/TutorialI/Misc/types.thy	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Misc/types.thy	Tue Apr 25 08:09:10 2000 +0200
@@ -7,7 +7,7 @@
 text{*\noindent\indexbold{*types}%
 Internally all synonyms are fully expanded.  As a consequence Isabelle's
 output never contains synonyms.  Their main purpose is to improve the
-readability of theory definitions.  Synonyms can be used just like any other
+readability of theories.  Synonyms can be used just like any other
 type:
 *}
 
@@ -28,7 +28,7 @@
 
 text{*\noindent%
 where \isacommand{defs}\indexbold{*defs} is a keyword and \isa{nand_def} and
-\isa{exor_def} are arbitrary user-supplied names.
+\isa{exor_def} are user-supplied names.
 The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
 that should only be used in constant definitions.
 Declarations and definitions can also be merged
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Recdef/Induction.thy
--- a/doc-src/TutorialI/Recdef/Induction.thy	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Induction.thy	Tue Apr 25 08:09:10 2000 +0200
@@ -15,7 +15,7 @@
 \textbf{recursion induction}. Roughly speaking, it
 requires you to prove for each \isacommand{recdef} equation that the property
 you are trying to establish holds for the left-hand side provided it holds
-for all recursive calls on the right-hand side. Here is a simple example:
+for all recursive calls on the right-hand side. Here is a simple example
 *}
 
 lemma "map f (sep(x,xs)) = sep(f x, map f xs)";
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Recdef/document/Induction.tex
--- a/doc-src/TutorialI/Recdef/document/Induction.tex	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Induction.tex	Tue Apr 25 08:09:10 2000 +0200
@@ -13,7 +13,7 @@
 \textbf{recursion induction}. Roughly speaking, it
 requires you to prove for each \isacommand{recdef} equation that the property
 you are trying to establish holds for the left-hand side provided it holds
-for all recursive calls on the right-hand side. Here is a simple example:%
+for all recursive calls on the right-hand side. Here is a simple example%
 \end{isamarkuptext}%
 \isacommand{lemma}~{"}map~f~(sep(x,xs))~=~sep(f~x,~map~f~xs){"}%
 \begin{isamarkuptxt}%
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Recdef/document/examples.tex
--- a/doc-src/TutorialI/Recdef/document/examples.tex	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/examples.tex	Tue Apr 25 08:09:10 2000 +0200
@@ -11,7 +11,7 @@
 \begin{isamarkuptext}%
 \noindent
 The definition of \isa{fib} is accompanied by a \bfindex{measure function}
-\isa{\isasymlambda{}n.$\;$n} that maps the argument of \isa{fib} to a
+\isa{\isasymlambda{}n.$\;$n} which maps the argument of \isa{fib} to a
 natural number. The requirement is that in each equation the measure of the
 argument on the left-hand side is strictly greater than the measure of the
 argument of each recursive call. In the case of \isa{fib} this is
@@ -74,7 +74,7 @@
 ~~{"}swap12~zs~~~~~~~=~zs{"}%
 \begin{isamarkuptext}%
 \noindent
-In the non-recursive case the termination measure degenerates to the empty
+For non-recursive functions the termination measure degenerates to the empty
 set \isa{\{\}}.%
 \end{isamarkuptext}%
 \end{isabelle}%
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Recdef/document/simplification.tex
--- a/doc-src/TutorialI/Recdef/document/simplification.tex	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex	Tue Apr 25 08:09:10 2000 +0200
@@ -42,10 +42,10 @@
 \begin{isamarkuptext}%
 \noindent
 Since the recursive call \isa{gcd(n, m mod n)} is no longer protected by
-an \isa{if}, this leads to an infinite chain of simplification steps.
+an \isa{if}, it is unfolded again, which leads to an infinite chain of simplification steps.
 Fortunately, this problem can be avoided in many different ways.
 
-Of course the most radical solution is to disable the offending
+The most radical solution is to disable the offending
 \isa{split_if} as shown in the section on case splits in
 \S\ref{sec:SimpFeatures}.
 However, we do not recommend this because it means you will often have to
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Recdef/document/termination.tex
--- a/doc-src/TutorialI/Recdef/document/termination.tex	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/termination.tex	Tue Apr 25 08:09:10 2000 +0200
@@ -4,8 +4,8 @@
 When a function is defined via \isacommand{recdef}, Isabelle tries to prove
 its termination with the help of the user-supplied measure.  All of the above
 examples are simple enough that Isabelle can prove automatically that the
-measure of the argument goes down in each recursive call. In that case
-$f$.\isa{simps} contains the defining equations (or variants derived from
+measure of the argument goes down in each recursive call. As a result,
+\isa{$f$.simps} will contain the defining equations (or variants derived from
 them) as theorems. For example, look (via \isacommand{thm}) at
 \isa{sep.simps} and \isa{sep1.simps} to see that they define the same
 function. What is more, those equations are automatically declared as
@@ -34,8 +34,8 @@
 \isacommand{apply}(arith)\isacommand{.}%
 \begin{isamarkuptext}%
 \noindent
-Because \isacommand{recdef}'s the termination prover involves simplification,
-we have declared our lemma a simplification rule. Therefore our second
+Because \isacommand{recdef}'s termination prover involves simplification,
+we have turned our lemma into a simplification rule. Therefore our second
 attempt to define our function will automatically take it into account:%
 \end{isamarkuptext}%
 \isacommand{consts}~g~::~{"}nat*nat~{\isasymRightarrow}~nat{"}\isanewline
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Recdef/examples.thy
--- a/doc-src/TutorialI/Recdef/examples.thy	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Recdef/examples.thy	Tue Apr 25 08:09:10 2000 +0200
@@ -14,7 +14,7 @@
 
 text{*\noindent
 The definition of \isa{fib} is accompanied by a \bfindex{measure function}
-\isa{\isasymlambda{}n.$\;$n} that maps the argument of \isa{fib} to a
+\isa{\isasymlambda{}n.$\;$n} which maps the argument of \isa{fib} to a
 natural number. The requirement is that in each equation the measure of the
 argument on the left-hand side is strictly greater than the measure of the
 argument of each recursive call. In the case of \isa{fib} this is
@@ -83,7 +83,7 @@
   "swap12 zs       = zs";
 
 text{*\noindent
-In the non-recursive case the termination measure degenerates to the empty
+For non-recursive functions the termination measure degenerates to the empty
 set \isa{\{\}}.
 *}
 
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Recdef/simplification.thy
--- a/doc-src/TutorialI/Recdef/simplification.thy	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Recdef/simplification.thy	Tue Apr 25 08:09:10 2000 +0200
@@ -49,10 +49,10 @@
 
 text{*\noindent
 Since the recursive call \isa{gcd(n, m mod n)} is no longer protected by
-an \isa{if}, this leads to an infinite chain of simplification steps.
+an \isa{if}, it is unfolded again, which leads to an infinite chain of simplification steps.
 Fortunately, this problem can be avoided in many different ways.
 
-Of course the most radical solution is to disable the offending
+The most radical solution is to disable the offending
 \isa{split_if} as shown in the section on case splits in
 \S\ref{sec:SimpFeatures}.
 However, we do not recommend this because it means you will often have to
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Recdef/termination.thy
--- a/doc-src/TutorialI/Recdef/termination.thy	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Recdef/termination.thy	Tue Apr 25 08:09:10 2000 +0200
@@ -6,8 +6,8 @@
 When a function is defined via \isacommand{recdef}, Isabelle tries to prove
 its termination with the help of the user-supplied measure.  All of the above
 examples are simple enough that Isabelle can prove automatically that the
-measure of the argument goes down in each recursive call. In that case
-$f$.\isa{simps} contains the defining equations (or variants derived from
+measure of the argument goes down in each recursive call. As a result,
+\isa{$f$.simps} will contain the defining equations (or variants derived from
 them) as theorems. For example, look (via \isacommand{thm}) at
 \isa{sep.simps} and \isa{sep1.simps} to see that they define the same
 function. What is more, those equations are automatically declared as
@@ -39,8 +39,8 @@
 apply(arith).;
 
 text{*\noindent
-Because \isacommand{recdef}'s the termination prover involves simplification,
-we have declared our lemma a simplification rule. Therefore our second
+Because \isacommand{recdef}'s termination prover involves simplification,
+we have turned our lemma into a simplification rule. Therefore our second
 attempt to define our function will automatically take it into account:
 *}
 
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/ToyList/ToyList.thy
--- a/doc-src/TutorialI/ToyList/ToyList.thy	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/ToyList/ToyList.thy	Tue Apr 25 08:09:10 2000 +0200
@@ -1,10 +1,10 @@
 theory ToyList = PreList:
 
 text{*\noindent
-HOL already has a predefined theory of lists called \texttt{List} ---
-\texttt{ToyList} is merely a small fragment of it chosen as an example. In
+HOL already has a predefined theory of lists called \isa{List} ---
+\isa{ToyList} is merely a small fragment of it chosen as an example. In
 contrast to what is recommended in \S\ref{sec:Basic:Theories},
-\texttt{ToyList} is not based on \texttt{Main} but on \texttt{PreList}, a
+\isa{ToyList} is not based on \isa{Main} but on \isa{PreList}, a
 theory that contains pretty much everything but lists, thus avoiding
 ambiguities caused by defining lists twice.
 *}
@@ -31,7 +31,7 @@
 
 \begin{warn}
   Syntax annotations are a powerful but completely optional feature. You
-  could drop them from theory \texttt{ToyList} and go back to the identifiers
+  could drop them from theory \isa{ToyList} and go back to the identifiers
   \isa{Nil} and \isa{Cons}. However, lists are such a central datatype
   that their syntax is highly customized. We recommend that novices should
   not use syntax annotations in their own theories.
@@ -67,7 +67,7 @@
 \isa{app} appends two lists and \isa{rev} reverses a list.  The keyword
 \isacommand{primrec}\index{*primrec} indicates that the recursion is of a
 particularly primitive kind where each recursive call peels off a datatype
-constructor from one of the arguments (see \S\ref{sec:datatype}).  Thus the
+constructor from one of the arguments.  Thus the
 recursion always terminates, i.e.\ the function is \bfindex{total}.
 
 The termination requirement is absolutely essential in HOL, a logic of total
@@ -103,7 +103,7 @@
 
 text{*\noindent
 When Isabelle prints a syntax error message, it refers to the HOL syntax as
-the \bfindex{inner syntax}.
+the \bfindex{inner syntax} and the enclosing theory language as the \bfindex{outer syntax}.
 
 
 \section{An introductory proof}
@@ -122,7 +122,7 @@
 
 theorem rev_rev [simp]: "rev(rev xs) = xs";
 
-txt{*\noindent\index{*theorem|bold}\index{*simp (attribute)|bold}
+txt{*\index{*theorem|bold}\index{*simp (attribute)|bold}
 \begin{itemize}
 \item
 establishes a new theorem to be proved, namely \isa{rev(rev xs) = xs},
@@ -220,8 +220,8 @@
 text{*
 \subsubsection*{First lemma: \texttt{rev(xs \at~ys) = (rev ys) \at~(rev xs)}}
 
-After abandoning the above proof attempt (at the shell level type
-\isa{oops}) we start a new proof:
+After abandoning the above proof attempt\indexbold{abandon proof} (at the shell level type
+\isacommand{oops}) we start a new proof:
 *}
 
 lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
@@ -232,7 +232,6 @@
 \emph{theorem}\index{theorem} and \emph{lemma}\index{lemma} pretty much
 interchangeably.
 
-%FIXME indent!
 There are two variables that we could induct on: \isa{xs} and
 \isa{ys}. Because \isa{\at} is defined by recursion on
 the first argument, \isa{xs} is the correct one:
@@ -251,9 +250,9 @@
 ~1.~rev~ys~=~rev~ys~@~[]\isanewline
 ~2. \dots
 \end{isabellepar}%
-We need to cancel this proof attempt and prove another simple lemma first.
-In the future the step of cancelling an incomplete proof before embarking on
-the proof of a lemma often remains implicit.
+Again, we need to abandon this proof attempt and prove another simple lemma first.
+In the future the step of abandoning an incomplete proof before embarking on
+the proof of a lemma usually remains implicit.
 *}
 (*<*)
 oops
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/ToyList/document/ToyList.tex
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Tue Apr 25 08:09:10 2000 +0200
@@ -2,10 +2,10 @@
 \isacommand{theory}~ToyList~=~PreList:%
 \begin{isamarkuptext}%
 \noindent
-HOL already has a predefined theory of lists called \texttt{List} ---
-\texttt{ToyList} is merely a small fragment of it chosen as an example. In
+HOL already has a predefined theory of lists called \isa{List} ---
+\isa{ToyList} is merely a small fragment of it chosen as an example. In
 contrast to what is recommended in \S\ref{sec:Basic:Theories},
-\texttt{ToyList} is not based on \texttt{Main} but on \texttt{PreList}, a
+\isa{ToyList} is not based on \isa{Main} but on \isa{PreList}, a
 theory that contains pretty much everything but lists, thus avoiding
 ambiguities caused by defining lists twice.%
 \end{isamarkuptext}%
@@ -31,7 +31,7 @@
 
 \begin{warn}
   Syntax annotations are a powerful but completely optional feature. You
-  could drop them from theory \texttt{ToyList} and go back to the identifiers
+  could drop them from theory \isa{ToyList} and go back to the identifiers
   \isa{Nil} and \isa{Cons}. However, lists are such a central datatype
   that their syntax is highly customized. We recommend that novices should
   not use syntax annotations in their own theories.
@@ -63,7 +63,7 @@
 \isa{app} appends two lists and \isa{rev} reverses a list.  The keyword
 \isacommand{primrec}\index{*primrec} indicates that the recursion is of a
 particularly primitive kind where each recursive call peels off a datatype
-constructor from one of the arguments (see \S\ref{sec:datatype}).  Thus the
+constructor from one of the arguments.  Thus the
 recursion always terminates, i.e.\ the function is \bfindex{total}.
 
 The termination requirement is absolutely essential in HOL, a logic of total
@@ -98,7 +98,7 @@
 \begin{isamarkuptext}%
 \noindent
 When Isabelle prints a syntax error message, it refers to the HOL syntax as
-the \bfindex{inner syntax}.
+the \bfindex{inner syntax} and the enclosing theory language as the \bfindex{outer syntax}.
 
 
 \section{An introductory proof}
@@ -116,7 +116,7 @@
 \end{isamarkuptext}%
 \isacommand{theorem}~rev\_rev~[simp]:~{"}rev(rev~xs)~=~xs{"}%
 \begin{isamarkuptxt}%
-\noindent\index{*theorem|bold}\index{*simp (attribute)|bold}
+\index{*theorem|bold}\index{*simp (attribute)|bold}
 \begin{itemize}
 \item
 establishes a new theorem to be proved, namely \isa{rev(rev xs) = xs},
@@ -209,8 +209,8 @@
 \begin{isamarkuptext}%
 \subsubsection*{First lemma: \texttt{rev(xs \at~ys) = (rev ys) \at~(rev xs)}}
 
-After abandoning the above proof attempt (at the shell level type
-\isa{oops}) we start a new proof:%
+After abandoning the above proof attempt\indexbold{abandon proof} (at the shell level type
+\isacommand{oops}) we start a new proof:%
 \end{isamarkuptext}%
 \isacommand{lemma}~rev\_app~[simp]:~{"}rev(xs~@~ys)~=~(rev~ys)~@~(rev~xs){"}%
 \begin{isamarkuptxt}%
@@ -220,7 +220,6 @@
 \emph{theorem}\index{theorem} and \emph{lemma}\index{lemma} pretty much
 interchangeably.
 
-%FIXME indent!
 There are two variables that we could induct on: \isa{xs} and
 \isa{ys}. Because \isa{\at} is defined by recursion on
 the first argument, \isa{xs} is the correct one:%
@@ -236,9 +235,9 @@
 ~1.~rev~ys~=~rev~ys~@~[]\isanewline
 ~2. \dots
 \end{isabellepar}%
-We need to cancel this proof attempt and prove another simple lemma first.
-In the future the step of cancelling an incomplete proof before embarking on
-the proof of a lemma often remains implicit.%
+Again, we need to abandon this proof attempt and prove another simple lemma first.
+In the future the step of abandoning an incomplete proof before embarking on
+the proof of a lemma usually remains implicit.%
 \end{isamarkuptxt}%
 %
 \begin{isamarkuptext}%
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Trie/Option2.thy
--- a/doc-src/TutorialI/Trie/Option2.thy	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Trie/Option2.thy	Tue Apr 25 08:09:10 2000 +0200
@@ -2,8 +2,7 @@
 theory Option2 = Main:;
 (*>*)
 
-datatype 'a option = None | Some 'a
-
+datatype 'a option = None | Some 'a;
 (*<*)
 end
 (*>*)
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Trie/Trie.thy
--- a/doc-src/TutorialI/Trie/Trie.thy	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Trie/Trie.thy	Tue Apr 25 08:09:10 2000 +0200
@@ -1,7 +1,6 @@
 (*<*)
 theory Trie = Main:;
 (*>*)
-
 text{*
 To minimize running time, each node of a trie should contain an array that maps
 letters to subtries. We have chosen a (sometimes) more space efficient
@@ -53,7 +52,7 @@
 *}
 
 lemma [simp]: "lookup (Trie None []) as = None";
-apply(cases "as", auto).;
+apply(case_tac as, auto).;
 
 text{*
 Things begin to get interesting with the definition of an update function
@@ -107,7 +106,7 @@
 The start of the proof is completely conventional:
 *}
 
-apply(induct_tac "as", auto);
+apply(induct_tac as, auto);
 
 txt{*\noindent
 Unfortunately, this time we are left with three intimidating looking subgoals:
@@ -127,8 +126,8 @@
 text{*\noindent
 Both \isaindex{case_tac} and \isaindex{induct_tac}
 take an optional first argument that specifies the range of subgoals they are
-applied to, where \isa{!} means all subgoals, i.e.\ \isa{[1-3]}. Individual
-subgoal number are also allowed.
+applied to, where \isa{!} means all subgoals, i.e.\ \isa{[1-3]} in our case. Individual
+subgoal numbers are also allowed.
 
 This proof may look surprisingly straightforward. However, note that this
 comes at a cost: the proof script is unreadable because the
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Trie/document/Option2.tex
--- a/doc-src/TutorialI/Trie/document/Option2.tex	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Trie/document/Option2.tex	Tue Apr 25 08:09:10 2000 +0200
@@ -1,4 +1,3 @@
 \begin{isabelle}%
 \isanewline
-\isacommand{datatype}~'a~option~=~None~|~Some~'a\isanewline
-\end{isabelle}%
+\isacommand{datatype}~'a~option~=~None~|~Some~'a\end{isabelle}%
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Trie/document/Trie.tex
--- a/doc-src/TutorialI/Trie/document/Trie.tex	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Trie/document/Trie.tex	Tue Apr 25 08:09:10 2000 +0200
@@ -44,7 +44,7 @@
 distinguishes the two cases whether the search string is empty or not:%
 \end{isamarkuptext}%
 \isacommand{lemma}~[simp]:~{"}lookup~(Trie~None~[])~as~=~None{"}\isanewline
-\isacommand{apply}(cases~{"}as{"},~auto)\isacommand{.}%
+\isacommand{apply}(case\_tac~as,~auto)\isacommand{.}%
 \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
@@ -93,7 +93,7 @@
 \isa{as} is instantiated.
 The start of the proof is completely conventional:%
 \end{isamarkuptxt}%
-\isacommand{apply}(induct\_tac~{"}as{"},~auto)%
+\isacommand{apply}(induct\_tac~as,~auto)%
 \begin{isamarkuptxt}%
 \noindent
 Unfortunately, this time we are left with three intimidating looking subgoals:
@@ -112,8 +112,8 @@
 \noindent
 Both \isaindex{case_tac} and \isaindex{induct_tac}
 take an optional first argument that specifies the range of subgoals they are
-applied to, where \isa{!} means all subgoals, i.e.\ \isa{[1-3]}. Individual
-subgoal number are also allowed.
+applied to, where \isa{!} means all subgoals, i.e.\ \isa{[1-3]} in our case. Individual
+subgoal numbers are also allowed.
 
 This proof may look surprisingly straightforward. However, note that this
 comes at a cost: the proof script is unreadable because the
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/appendix.tex
--- a/doc-src/TutorialI/appendix.tex	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/appendix.tex	Tue Apr 25 08:09:10 2000 +0200
@@ -80,7 +80,7 @@
 \end{center}
 \caption{Mathematical symbols and their ASCII-equivalents}
 \label{fig:ascii}
-\end{figure}
+\end{figure}\indexbold{ASCII symbols}
 
 \begin{figure}[htbp]
 \begin{center}
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/basics.tex
--- a/doc-src/TutorialI/basics.tex	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/basics.tex	Tue Apr 25 08:09:10 2000 +0200
@@ -48,13 +48,13 @@
 where \texttt{B}$@1$, \dots, \texttt{B}$@n$ are the names of existing
 theories that \texttt{T} is based on and \texttt{\textit{declarations,
     definitions, and proofs}} represents the newly introduced concepts
-(types, functions etc) and proofs about them. The \texttt{B}$@i$ are the
+(types, functions etc.) and proofs about them. The \texttt{B}$@i$ are the
 direct \textbf{parent theories}\indexbold{parent theory} of \texttt{T}.
 Everything defined in the parent theories (and their parents \dots) is
 automatically visible. To avoid name clashes, identifiers can be
 \textbf{qualified} by theory names as in \texttt{T.f} and
 \texttt{B.f}.\indexbold{identifier!qualified} Each theory \texttt{T} must
-reside in a \indexbold{theory file} named \texttt{T.thy}.
+reside in a \bfindex{theory file} named \texttt{T.thy}.
 
 This tutorial is concerned with introducing you to the different linguistic
 constructs that can fill \textit{\texttt{declarations, definitions, and
@@ -74,59 +74,33 @@
 \end{warn}
 
 
-\section{Interaction and interfaces}
-
-Interaction with Isabelle can either occur at the shell level or through more
-advanced interfaces. To keep the tutorial independent of the interface we
-have phrased the description of the intraction in a neutral language. For
-example, the phrase ``to cancel a proof'' means to type \texttt{oops} at the
-shell level, which is explained the first time the phrase is used. Other
-interfaces perform the same act by cursor movements and/or mouse clicks.
-Although shell-based interaction is quite feasible for the kind of proof
-scripts currently presented in this tutorial, the recommended interface for
-Isabelle/Isar is the Emacs-based \bfindex{Proof
-  General}~\cite{Aspinall:TACAS:2000,proofgeneral}.
-
-To improve readability some of the interfaces (including the shell level)
-offer special fonts with mathematical symbols. Therefore the usual
-mathematical symbols are used throughout the tutorial. Their
-ASCII-equivalents are shown in figure~\ref{fig:ascii} in the appendix.
-
-Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} Some interfaces,
-for example Proof General, require each command to be terminated by a
-semicolon, whereas others, for example the shell level, do not. But even at
-the shell level it is advisable to use semicolons to enforce that a command
-is executed immediately; otherwise Isabelle may wait for the next keyword
-before it knows that the command is complete. Note that for readibility
-reasons we often drop the final semicolon in the text.
-
-
 \section{Types, terms and formulae}
 \label{sec:TypesTermsForms}
 \indexbold{type}
 
-Embedded in the declarations of a theory are the types, terms and formulae of
-HOL. HOL is a typed logic whose type system resembles that of functional
-programming languages like ML or Haskell. Thus there are
+Embedded in a theory are the types, terms and formulae of HOL. HOL is a typed
+logic whose type system resembles that of functional programming languages
+like ML or Haskell. Thus there are
 \begin{description}
-\item[base types,] in particular \ttindex{bool}, the type of truth values,
-and \ttindex{nat}, the type of natural numbers.
-\item[type constructors,] in particular \texttt{list}, the type of
-lists, and \texttt{set}, the type of sets. Type constructors are written
-postfix, e.g.\ \texttt{(nat)list} is the type of lists whose elements are
+\item[base types,] in particular \isaindex{bool}, the type of truth values,
+and \isaindex{nat}, the type of natural numbers.
+\item[type constructors,] in particular \isaindex{list}, the type of
+lists, and \isaindex{set}, the type of sets. Type constructors are written
+postfix, e.g.\ \isa{(nat)list} is the type of lists whose elements are
 natural numbers. Parentheses around single arguments can be dropped (as in
-\texttt{nat list}), multiple arguments are separated by commas (as in
-\texttt{(bool,nat)foo}).
+\isa{nat list}), multiple arguments are separated by commas (as in
+\isa{(bool,nat)ty}).
 \item[function types,] denoted by \isasymFun\indexbold{$IsaFun@\isasymFun}.
-  In HOL \isasymFun\ represents {\em total} functions only. As is customary,
-  \texttt{$\tau@1$ \isasymFun~$\tau@2$ \isasymFun~$\tau@3$} means
-  \texttt{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also
-  supports the notation \texttt{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$}
-  which abbreviates \texttt{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$
+  In HOL \isasymFun\ represents \emph{total} functions only. As is customary,
+  \isa{$\tau@1$ \isasymFun~$\tau@2$ \isasymFun~$\tau@3$} means
+  \isa{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also
+  supports the notation \isa{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$}
+  which abbreviates \isa{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$
     \isasymFun~$\tau$}.
-\item[type variables,] denoted by \texttt{'a}, \texttt{'b} etc, just like in
-ML. They give rise to polymorphic types like \texttt{'a \isasymFun~'a}, the
-type of the identity function.
+\item[type variables,]\indexbold{type variable}\indexbold{variable!type}
+  denoted by \isaindexbold{'a}, \isa{'b} etc., just like in ML. They give rise
+  to polymorphic types like \isa{'a \isasymFun~'a}, the type of the identity
+  function.
 \end{description}
 \begin{warn}
   Types are extremely important because they prevent us from writing
@@ -145,77 +119,71 @@
 
 \noindent
 This can be reversed by \texttt{ML "reset show_types"}. Various other flags
-can be set and reset in the same manner.\bfindex{flag!(re)setting}
+can be set and reset in the same manner.\indexbold{flag!(re)setting}
 \end{warn}
 
 
 \textbf{Terms}\indexbold{term} are formed as in functional programming by
-applying functions to arguments. If \texttt{f} is a function of type
-\texttt{$\tau@1$ \isasymFun~$\tau@2$} and \texttt{t} is a term of type
-$\tau@1$ then \texttt{f~t} is a term of type $\tau@2$. HOL also supports
-infix functions like \texttt{+} and some basic constructs from functional
+applying functions to arguments. If \isa{f} is a function of type
+\isa{$\tau@1$ \isasymFun~$\tau@2$} and \isa{t} is a term of type
+$\tau@1$ then \isa{f~t} is a term of type $\tau@2$. HOL also supports
+infix functions like \isa{+} and some basic constructs from functional
 programming:
 \begin{description}
-\item[\texttt{if $b$ then $t@1$ else $t@2$}]\indexbold{*if}
+\item[\isa{if $b$ then $t@1$ else $t@2$}]\indexbold{*if}
 means what you think it means and requires that
-$b$ is of type \texttt{bool} and $t@1$ and $t@2$ are of the same type.
-\item[\texttt{let $x$ = $t$ in $u$}]\indexbold{*let}
+$b$ is of type \isa{bool} and $t@1$ and $t@2$ are of the same type.
+\item[\isa{let $x$ = $t$ in $u$}]\indexbold{*let}
 is equivalent to $u$ where all occurrences of $x$ have been replaced by
 $t$. For example,
-\texttt{let x = 0 in x+x} means \texttt{0+0}. Multiple bindings are separated
-by semicolons: \texttt{let $x@1$ = $t@1$; \dots; $x@n$ = $t@n$ in $u$}.
-\item[\texttt{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}]
+\isa{let x = 0 in x+x} is equivalent to \isa{0+0}. Multiple bindings are separated
+by semicolons: \isa{let $x@1$ = $t@1$; \dots; $x@n$ = $t@n$ in $u$}.
+\item[\isa{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}]
 \indexbold{*case}
-evaluates to $e@i$ if $e$ is of the form
-$c@i$. See~\S\ref{sec:case-expressions} for details.
+evaluates to $e@i$ if $e$ is of the form $c@i$.
 \end{description}
 
 Terms may also contain
 \isasymlambda-abstractions\indexbold{$Isalam@\isasymlambda}. For example,
-\texttt{\isasymlambda{}x.~x+1} is the function that takes an argument
-\texttt{x} and returns \texttt{x+1}. Instead of
-\texttt{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.}~$t$ we can write
-\texttt{\isasymlambda{}x~y~z.}~$t$.
+\isa{\isasymlambda{}x.~x+1} is the function that takes an argument \isa{x} and
+returns \isa{x+1}. Instead of
+\isa{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.~$t$} we can write
+\isa{\isasymlambda{}x~y~z.~$t$}.
 
-\textbf{Formulae}\indexbold{formula}
-are terms of type \texttt{bool}. There are the basic
-constants \ttindexbold{True} and \ttindexbold{False} and the usual logical
-connectives (in decreasing order of priority):
-\indexboldpos{\isasymnot}{$HOL0not},
-\indexboldpos{\isasymand}{$HOL0and},
-\indexboldpos{\isasymor}{$HOL0or}, and
-\indexboldpos{\isasymimp}{$HOL0imp},
+\textbf{Formulae}\indexbold{formula} are terms of type \isaindexbold{bool}.
+There are the basic constants \isaindexbold{True} and \isaindexbold{False} and
+the usual logical connectives (in decreasing order of priority):
+\indexboldpos{\isasymnot}{$HOL0not}, \indexboldpos{\isasymand}{$HOL0and},
+\indexboldpos{\isasymor}{$HOL0or}, and \indexboldpos{\isasymimp}{$HOL0imp},
 all of which (except the unary \isasymnot) associate to the right. In
-particular \texttt{A \isasymimp~B \isasymimp~C} means
-\texttt{A \isasymimp~(B \isasymimp~C)} and is thus
-logically equivalent with \texttt{A \isasymand~B \isasymimp~C}
-(which is \texttt{(A \isasymand~B) \isasymimp~C}).
+particular \isa{A \isasymimp~B \isasymimp~C} means \isa{A \isasymimp~(B
+  \isasymimp~C)} and is thus logically equivalent to \isa{A \isasymand~B
+  \isasymimp~C} (which is \isa{(A \isasymand~B) \isasymimp~C}).
 
 Equality is available in the form of the infix function
-\texttt{=}\indexbold{$HOL0eq@\texttt{=}} of type \texttt{'a \isasymFun~'a
-  \isasymFun~bool}. Thus \texttt{$t@1$ = $t@2$} is a formula provided $t@1$
+\isa{=}\indexbold{$HOL0eq@\texttt{=}} of type \isa{'a \isasymFun~'a
+  \isasymFun~bool}. Thus \isa{$t@1$ = $t@2$} is a formula provided $t@1$
 and $t@2$ are terms of the same type. In case $t@1$ and $t@2$ are of type
-\texttt{bool}, \texttt{=} acts as if-and-only-if. The formula
-$t@1$~\isasymnoteq~$t@2$ is merely an abbreviation for
-\texttt{\isasymnot($t@1$ = $t@2$)}.
+\isa{bool}, \isa{=} acts as if-and-only-if. The formula
+\isa{$t@1$~\isasymnoteq~$t@2$} is merely an abbreviation for
+\isa{\isasymnot($t@1$ = $t@2$)}.
 
 The syntax for quantifiers is
-\texttt{\isasymforall{}x.}~$P$\indexbold{$HOL0All@\isasymforall} and
-\texttt{\isasymexists{}x.}~$P$\indexbold{$HOL0Ex@\isasymexists}.  There is
-even \texttt{\isasymuniqex{}x.}~$P$\index{$HOL0ExU@\isasymuniqex|bold}, which
-means that there exists exactly one \texttt{x} that satisfies $P$.
-Nested quantifications can be abbreviated:
-\texttt{\isasymforall{}x~y~z.}~$P$ means
-\texttt{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.}~$P$.
+\isa{\isasymforall{}x.~$P$}\indexbold{$HOL0All@\isasymforall} and
+\isa{\isasymexists{}x.~$P$}\indexbold{$HOL0Ex@\isasymexists}.  There is
+even \isa{\isasymuniqex{}x.~$P$}\index{$HOL0ExU@\isasymuniqex|bold}, which
+means that there exists exactly one \isa{x} that satisfies \isa{$P$}.  Nested
+quantifications can be abbreviated: \isa{\isasymforall{}x~y~z.~$P$} means
+\isa{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.~$P$}.
 
 Despite type inference, it is sometimes necessary to attach explicit
-\bfindex{type constraints} to a term.  The syntax is \texttt{$t$::$\tau$} as
-in \texttt{x < (y::nat)}. Note that \ttindexboldpos{::}{$Isalamtc} binds weakly
-and should therefore be enclosed in parentheses: \texttt{x < y::nat} is
-ill-typed because it is interpreted as \texttt{(x < y)::nat}. The main reason
-for type constraints are overloaded functions like \texttt{+}, \texttt{*} and
-\texttt{<}. (See \S\ref{sec:TypeClasses} for a full discussion of
-overloading.)
+\textbf{type constraints}\indexbold{type constraint} to a term.  The syntax is
+\isa{$t$::$\tau$} as in \isa{x < (y::nat)}. Note that
+\ttindexboldpos{::}{$Isalamtc} binds weakly and should therefore be enclosed
+in parentheses: \isa{x < y::nat} is ill-typed because it is interpreted as
+\isa{(x < y)::nat}. The main reason for type constraints are overloaded
+functions like \isa{+}, \isa{*} and \isa{<}. (See \S\ref{sec:TypeClasses} for
+a full discussion of overloading.)
 
 \begin{warn}
 In general, HOL's concrete syntax tries to follow the conventions of
@@ -234,33 +202,35 @@
 
 \begin{itemize}
 \item
-Remember that \texttt{f t u} means \texttt{(f t) u} and not \texttt{f(t u)}!
+Remember that \isa{f t u} means \isa{(f t) u} and not \isa{f(t u)}!
 \item
-Isabelle allows infix functions like \texttt{+}. The prefix form of function
-application binds more strongly than anything else and hence \texttt{f~x + y}
-means \texttt{(f~x)~+~y} and not \texttt{f(x+y)}.
+Isabelle allows infix functions like \isa{+}. The prefix form of function
+application binds more strongly than anything else and hence \isa{f~x + y}
+means \isa{(f~x)~+~y} and not \isa{f(x+y)}.
 \item Remember that in HOL if-and-only-if is expressed using equality.  But
   equality has a high priority, as befitting a relation, while if-and-only-if
-  typically has the lowest priority.  Thus, \texttt{\isasymnot~\isasymnot~P =
-    P} means \texttt{\isasymnot\isasymnot(P = P)} and not
-  \texttt{(\isasymnot\isasymnot P) = P}. When using \texttt{=} to mean
-  logical equivalence, enclose both operands in parentheses, as in \texttt{(A
+  typically has the lowest priority.  Thus, \isa{\isasymnot~\isasymnot~P =
+    P} means \isa{\isasymnot\isasymnot(P = P)} and not
+  \isa{(\isasymnot\isasymnot P) = P}. When using \isa{=} to mean
+  logical equivalence, enclose both operands in parentheses, as in \isa{(A
     \isasymand~B) = (B \isasymand~A)}.
 \item
 Constructs with an opening but without a closing delimiter bind very weakly
 and should therefore be enclosed in parentheses if they appear in subterms, as
-in \texttt{f = (\isasymlambda{}x.~x)}. This includes \ttindex{if},
-\ttindex{let}, \ttindex{case}, \isasymlambda, and quantifiers.
+in \isa{f = (\isasymlambda{}x.~x)}. This includes \isaindex{if},
+\isaindex{let}, \isaindex{case}, \isa{\isasymlambda}, and quantifiers.
 \item
-Never write \texttt{\isasymlambda{}x.x} or \texttt{\isasymforall{}x.x=x}
-because \texttt{x.x} is always read as a single qualified identifier that
-refers to an item \texttt{x} in theory \texttt{x}. Write
-\texttt{\isasymlambda{}x.~x} and \texttt{\isasymforall{}x.~x=x} instead.
-\item Identifiers\indexbold{identifier} may contain \texttt{_} and \texttt{'}.
+Never write \isa{\isasymlambda{}x.x} or \isa{\isasymforall{}x.x=x}
+because \isa{x.x} is always read as a single qualified identifier that
+refers to an item \isa{x} in theory \isa{x}. Write
+\isa{\isasymlambda{}x.~x} and \isa{\isasymforall{}x.~x=x} instead.
+\item Identifiers\indexbold{identifier} may contain \isa{_} and \isa{'}.
 \end{itemize}
 
-Remember that ASCII-equivalents of all mathematical symbols are
-given in figure~\ref{fig:ascii} in the appendix.
+For the sake of readability the usual mathematical symbols are used throughout
+the tutorial. Their ASCII-equivalents are shown in figure~\ref{fig:ascii} in
+the appendix.
+
 
 \section{Variables}
 \label{sec:variables}
@@ -270,9 +240,9 @@
 variables are automatically renamed to avoid clashes with free variables. In
 addition, Isabelle has a third kind of variable, called a \bfindex{schematic
   variable}\indexbold{variable!schematic} or \bfindex{unknown}, which starts
-with a \texttt{?}.  Logically, an unknown is a free variable. But it may be
+with a \isa{?}.  Logically, an unknown is a free variable. But it may be
 instantiated by another term during the proof process. For example, the
-mathematical theorem $x = x$ is represented in Isabelle as \texttt{?x = ?x},
+mathematical theorem $x = x$ is represented in Isabelle as \isa{?x = ?x},
 which means that Isabelle can instantiate it arbitrarily. This is in contrast
 to ordinary variables, which remain fixed. The programming language Prolog
 calls unknowns {\em logical\/} variables.
@@ -283,11 +253,37 @@
 indicates that Isabelle will automatically instantiate those unknowns
 suitably when the theorem is used in some other proof.
 \begin{warn}
-  If you use \texttt{?}\index{$HOL0Ex@\texttt{?}} as an existential
-  quantifier, it needs to be followed by a space. Otherwise \texttt{?x} is
+  If you use \isa{?}\index{$HOL0Ex@\texttt{?}} as an existential
+  quantifier, it needs to be followed by a space. Otherwise \isa{?x} is
   interpreted as a schematic variable.
 \end{warn}
 
+\section{Interaction and interfaces}
+
+Interaction with Isabelle can either occur at the shell level or through more
+advanced interfaces. To keep the tutorial independent of the interface we
+have phrased the description of the intraction in a neutral language. For
+example, the phrase ``to abandon a proof'' means to type \isacommand{oops} at the
+shell level, which is explained the first time the phrase is used. Other
+interfaces perform the same act by cursor movements and/or mouse clicks.
+Although shell-based interaction is quite feasible for the kind of proof
+scripts currently presented in this tutorial, the recommended interface for
+Isabelle/Isar is the Emacs-based \bfindex{Proof
+  General}~\cite{Aspinall:TACAS:2000,proofgeneral}.
+
+Some interfaces (including the shell level) offer special fonts with
+mathematical symbols. For those that do not, remember that ASCII-equivalents
+are shown in figure~\ref{fig:ascii} in the appendix.
+
+Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} Some interfaces,
+for example Proof General, require each command to be terminated by a
+semicolon, whereas others, for example the shell level, do not. But even at
+the shell level it is advisable to use semicolons to enforce that a command
+is executed immediately; otherwise Isabelle may wait for the next keyword
+before it knows that the command is complete. Note that for readibility
+reasons we often drop the final semicolon in the text.
+
+
 \section{Getting started}
 
 Assuming you have installed Isabelle, you start it by typing \texttt{isabelle
@@ -299,4 +295,4 @@
 create theory files.  While you are developing a theory, we recommend to
 type each command into the file first and then enter it into Isabelle by
 copy-and-paste, thus ensuring that you have a complete record of your theory.
-As mentioned earlier, Proof General offers a much superior interface.
+As mentioned above, Proof General offers a much superior interface.
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/fp.tex
--- a/doc-src/TutorialI/fp.tex	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/fp.tex	Tue Apr 25 08:09:10 2000 +0200
@@ -116,14 +116,13 @@
   \isacommand{typ}\indexbold{*typ} \textit{string} reads and prints the given
   string as a type in the current context.
 \item[(Re)loading theories:] When you start your interaction you must open a
-  named theory with the line
-  \isacommand{theory}\texttt{~T~=}~\dots~\texttt{:}. Isabelle automatically
-  loads all the required parent theories from their respective files (which
-  may take a moment, unless the theories are already loaded and the files
-  have not been modified). The only time when you need to load a theory by
-  hand is when you simply want to check if it loads successfully without
-  wanting to make use of the theory itself. This you can do by typing
-  \isacommand{use\_thy}\indexbold{*use_thy}~\texttt{"T"}.
+  named theory with the line \isa{\isacommand{theory}~T~=~\dots~:}. Isabelle
+  automatically loads all the required parent theories from their respective
+  files (which may take a moment, unless the theories are already loaded and
+  the files have not been modified). The only time when you need to load a
+  theory by hand is when you simply want to check if it loads successfully
+  without wanting to make use of the theory itself. This you can do by typing
+  \isa{\isacommand{use\_thy}\indexbold{*use_thy}~"T"}.
   
   If you suddenly discover that you need to modify a parent theory of your
   current theory you must first abandon your current theory (at the shell
@@ -134,6 +133,9 @@
 \end{description}
 Further commands are found in the Isabelle/Isar Reference Manual.
 
+We now examine Isabelle's functional programming constructs systematically,
+starting with inductive datatypes.
+
 
 \section{Datatypes}
 \label{sec:datatype}
@@ -149,12 +151,12 @@
 
 Lists are one of the essential datatypes in computing. Readers of this
 tutorial and users of HOL need to be familiar with their basic operations.
-Theory \texttt{ToyList} is only a small fragment of HOL's predefined theory
-\texttt{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}.
+Theory \isa{ToyList} is only a small fragment of HOL's predefined theory
+\isa{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}.
 The latter contains many further operations. For example, the functions
-\isaindexbold{hd} (`head') and \isaindexbold{tl} (`tail') return the first
+\isaindexbold{hd} (``head'') and \isaindexbold{tl} (``tail'') return the first
 element and the remainder of a list. (However, pattern-matching is usually
-preferable to \isa{hd} and \isa{tl}.)  Theory \texttt{List} also contains
+preferable to \isa{hd} and \isa{tl}.)  Theory \isa{List} also contains
 more syntactic sugar: \isa{[}$x@1$\isa{,}\dots\isa{,}$x@n$\isa{]} abbreviates
 $x@1$\isa{\#}\dots\isa{\#}$x@n$\isa{\#[]}.  In the rest of the tutorial we
 always use HOL's predefined lists.
@@ -169,7 +171,7 @@
 C@1~\tau@{11}~\dots~\tau@{1k@1} ~\mid~ \dots ~\mid~
 C@m~\tau@{m1}~\dots~\tau@{mk@m}
 \]
-where $\alpha@i$ are type variables (the parameters), $C@i$ are distinct
+where $\alpha@i$ are distinct type variables (the parameters), $C@i$ are distinct
 constructor names and $\tau@{ij}$ are types; it is customary to capitalize
 the first letter in constructor names. There are a number of
 restrictions (such as that the type should not be empty) detailed
@@ -192,7 +194,7 @@
 Isabelle immediately sees that $f$ terminates because one (fixed!) argument
 becomes smaller with every recursive call. There must be exactly one equation
 for each constructor.  Their order is immaterial.
-A more general method for defining total recursive functions is explained in
+A more general method for defining total recursive functions is introduced in
 \S\ref{sec:recdef}.
 
 \begin{exercise}
@@ -276,6 +278,7 @@
 the constructs introduced above.
 
 \input{Ifexpr/document/Ifexpr.tex}
+\medskip
 
 How does one come up with the required lemmas? Try to prove the main theorems
 without them and study carefully what \isa{auto} leaves unproved. This has
@@ -368,7 +371,7 @@
 
 \subsection{Products}
 
-HOL also has pairs: \isa{($a@1$,$a@2$)} is of type \texttt{$\tau@1$ *
+HOL also has pairs: \isa{($a@1$,$a@2$)} is of type \isa{$\tau@1$ *
   $\tau@2$} provided each $a@i$ is of type $\tau@i$. The components of a pair
 are extracted by \isa{fst} and \isa{snd}: \isa{fst($x$,$y$) = $x$} and
 \isa{snd($x$,$y$) = $y$}. Tuples are simulated by pairs nested to the right:
@@ -411,7 +414,7 @@
 
 
 \subsection{Type synonyms}
-\indexbold{type synonyms}
+\indexbold{type synonym}
 
 Type synonyms are similar to those found in ML. Their syntax is fairly self
 explanatory:
@@ -420,7 +423,6 @@
 
 Note that pattern-matching is not allowed, i.e.\ each definition must be of
 the form $f\,x@1\,\dots\,x@n~\isasymequiv~t$.
-
 Section~\S\ref{sec:Simplification} explains how definitions are used
 in proofs.
 
@@ -434,17 +436,17 @@
 \chapter{More Functional Programming}
 
 The purpose of this chapter is to deepen the reader's understanding of the
-concepts encountered so far and to introduce an advanced forms of datatypes
-and recursive functions. The first two sections give a structured
-presentation of theorem proving by simplification
-(\S\ref{sec:Simplification}) and discuss important heuristics for induction
-(\S\ref{sec:InductionHeuristics}). They can be skipped by readers less
-interested in proofs. They are followed by a case study, a compiler for
-expressions (\S\ref{sec:ExprCompiler}). Advanced datatypes, including those
-involving function spaces, are covered in \S\ref{sec:advanced-datatypes},
-which closes with another case study, search trees (``tries'').  Finally we
-introduce a very general form of recursive function definition which goes
-well beyond what \isacommand{primrec} allows (\S\ref{sec:recdef}).
+concepts encountered so far and to introduce advanced forms of datatypes and
+recursive functions. The first two sections give a structured presentation of
+theorem proving by simplification (\S\ref{sec:Simplification}) and discuss
+important heuristics for induction (\S\ref{sec:InductionHeuristics}). They can
+be skipped by readers less interested in proofs. They are followed by a case
+study, a compiler for expressions (\S\ref{sec:ExprCompiler}). Advanced
+datatypes, including those involving function spaces, are covered in
+\S\ref{sec:advanced-datatypes}, which closes with another case study, search
+trees (``tries'').  Finally we introduce \isacommand{recdef}, a very general
+form of recursive function definition which goes well beyond what
+\isacommand{primrec} allows (\S\ref{sec:recdef}).
 
 
 \section{Simplification}
@@ -478,7 +480,7 @@
 (0#1#[]) @ []  \(\leadsto\)  0#((1#[]) @ [])  \(\leadsto\)  0#(1#([] @ []))  \(\leadsto\)  0#1#[]
 \end{ttbox}
 This is also known as \bfindex{term rewriting} and the equations are referred
-to as \bfindex{rewrite rules}. This is more honest than ``simplification''
+to as \bfindex{rewrite rules}. ``Rewriting'' is more honest than ``simplification''
 because the terms do not necessarily become simpler in the process.
 
 \subsubsection{Simplification rules}
@@ -487,7 +489,7 @@
 To facilitate simplification, theorems can be declared to be simplification
 rules (with the help of the attribute \isa{[simp]}\index{*simp
   (attribute)}), in which case proofs by simplification make use of these
-rules by default. In addition the constructs \isacommand{datatype} and
+rules automatically. In addition the constructs \isacommand{datatype} and
 \isacommand{primrec} (and a few others) invisibly declare useful
 simplification rules. Explicit definitions are \emph{not} declared
 simplification rules automatically!
@@ -502,14 +504,14 @@
 theorems [simp] = \(list of theorem names\);
 theorems [simp del] = \(list of theorem names\);
 \end{ttbox}
-As a rule of thumb, rules that really simplify (like \isa{rev(rev xs) =
+As a rule of thumb, equations that really simplify (like \isa{rev(rev xs) =
   xs} and \mbox{\isa{xs \at\ [] = xs}}) should be made simplification
 rules.  Those of a more specific nature (e.g.\ distributivity laws, which
 alter the structure of terms considerably) should only be used selectively,
 i.e.\ they should not be default simplification rules.  Conversely, it may
 also happen that a simplification rule needs to be disabled in certain
 proofs.  Frequent changes in the simplification status of a theorem may
-indicates a badly designed theory.
+indicate a badly designed theory.
 \begin{warn}
   Simplification may not terminate, for example if both $f(x) = g(x)$ and
   $g(x) = f(x)$ are simplification rules. It is the user's responsibility not
@@ -568,7 +570,7 @@
 
 Proving a goal containing \isaindex{let}-expressions almost invariably
 requires the \isa{let}-con\-structs to be expanded at some point. Since
-\isa{let}-\isa{in} is just syntactic sugar for a defined constant (called
+\isa{let}-\isa{in} is just syntactic sugar for a predefined constant (called
 \isa{Let}), expanding \isa{let}-constructs means rewriting with
 \isa{Let_def}:
 
@@ -600,7 +602,7 @@
 \index{arithmetic}
 
 The simplifier routinely solves a small class of linear arithmetic formulae
-(over types \isa{nat} and \isa{int}): it only takes into account
+(over type \isa{nat} and other numeric types): it only takes into account
 assumptions and conclusions that are (possibly negated) (in)equalities
 (\isa{=}, \isasymle, \isa{<}) and it only knows about addition. Thus
 
@@ -673,7 +675,7 @@
 \end{quote}
 The heuristic is tricky to apply because it is not obvious that
 \isa{rev xs \at\ ys} is simpler than \isa{itrev xs ys}. But see what
-happens if you try to prove the symmetric equation!
+happens if you try to prove \isa{rev xs \at\ ys = itrev xs ys}!
 
 
 \section{Case study: compiling expressions}
@@ -719,6 +721,7 @@
 right of a function arrow, but never on the left. Hence the above can of worms
 is ruled out but the following example of a potentially infinitely branching tree is
 accepted:
+\smallskip
 
 \input{Datatype/document/Fundata.tex}
 \bigskip
@@ -728,7 +731,7 @@
 \begin{ttbox}
 datatype lam = C (lam -> lam)
 \end{ttbox}
-do indeed make sense (note the intentionally different arrow \isa{->}!).
+do indeed make sense (note the intentionally different arrow \isa{->}).
 There is even a version of LCF on top of HOL, called
 HOLCF~\cite{MuellerNvOS99}.
 
@@ -785,11 +788,11 @@
 Proper tries associate some value with each string. Since the
 information is stored only in the final node associated with the string, many
 nodes do not carry any value. This distinction is captured by the
-following predefined datatype (from theory \texttt{Option}, which is a parent
-of \texttt{Main}):
+following predefined datatype (from theory \isa{Option}, which is a parent
+of \isa{Main}):
+\smallskip
 \input{Trie/document/Option2.tex}
-\indexbold{*option}\indexbold{*None}\indexbold{*Some}
-
+\indexbold{*option}\indexbold{*None}\indexbold{*Some}%
 \input{Trie/document/Trie.tex}
 
 \begin{exercise}
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/isabelle.sty
--- a/doc-src/TutorialI/isabelle.sty	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/isabelle.sty	Tue Apr 25 08:09:10 2000 +0200
@@ -19,6 +19,9 @@
 
 \newcommand{\isa}[1]{\emph{\isabelledefaultstyle\isabellestyle #1}}
 
+\newenvironment{isabellequote}%
+{\begin{quote}\begin{isabelle}\noindent}{\end{isabelle}\end{quote}}
+
 \newcommand{\isanewline}{\mbox{}\\\mbox{}}
 
 \chardef\isabraceleft=`\{