*** empty log message ***

--- a/doc-src/TutorialI/Advanced/advanced.tex	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Advanced/advanced.tex	Mon Oct 09 10:18:21 2000 +0200
@@ -1,5 +1,5 @@
 \chapter{Advanced Simplification, Recursion, and Induction}
-\markboth{}{CHAPTER 4: ADVANCED}
+\markboth{}{CHAPTER 4: ADVANCED SIMPLIFICATION ...}
 
 Although we have already learned a lot about simplification, recursion and
 induction, there are some advanced proof techniques that we have not covered

--- a/doc-src/TutorialI/CTL/CTL.thy	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/CTL/CTL.thy	Mon Oct 09 10:18:21 2000 +0200
@@ -291,12 +291,13 @@
 text{*
 Function @{term path} has fulfilled its purpose now and can be forgotten
 about. It was merely defined to provide the witness in the proof of the
-@{thm[source]infinity_lemma}. Afficionados of minimal proofs might like to know
+@{thm[source]infinity_lemma}. Aficionados of minimal proofs might like to know
 that we could have given the witness without having to define a new function:
 the term
 @{term[display]"nat_rec s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> P u)"}
+is extensionally equal to @{term"path s P"},
 where @{term nat_rec} is the predefined primitive recursor on @{typ nat}, whose defining
-equations we omit, is extensionally equal to @{term"path s P"}.
+equations we omit.
 *};
 (*<*)
 lemma infinity_lemma:
@@ -372,6 +373,18 @@
 done
 
 text{*
+The above language is not quite CTL. The latter also includes an
+until-operator, usually written as an infix @{text U}. The formula
+@{term"f U g"} means ``@{term f} until @{term g}''.
+It is not definable in terms of the other operators!
+\begin{exercise}
+Extend the datatype of formulae by the until operator with semantics
+@{text[display]"s \<Turnstile> f U g = (............)"}
+and model checking algorithm
+@{text[display]"mc(f U g) = (............)"}
+Prove that the equivalence between semantics and model checking still holds.
+\end{exercise}
+
 Let us close this section with a few words about the executability of @{term mc}.
 It is clear that if all sets are finite, they can be represented as lists and the usual
 set operations are easily implemented. Only @{term lfp} requires a little thought.

--- a/doc-src/TutorialI/CTL/PDL.thy	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/CTL/PDL.thy	Mon Oct 09 10:18:21 2000 +0200
@@ -187,4 +187,34 @@
 apply(induct_tac f);
 apply(auto simp add:EF_lemma);
 done;
-(*<*)end(*>*)
+
+text{*
+\begin{exercise}
+@{term AX} has a dual operator @{term EN}\footnote{We cannot use the customary @{text EX}
+as that is the ASCII equivalent of @{text"\<exists>"}}
+(``there exists a next state such that'') with the intended semantics
+@{prop[display]"(s \<Turnstile> EN f) = (EX t. (s,t) : M & t \<Turnstile> f)"}
+Fortunately, @{term"EN f"} can already be expressed as a PDL formula. How?
+
+Show that the semantics for @{term EF} satisfies the following recursion equation:
+@{prop[display]"(s \<Turnstile> EF f) = (s \<Turnstile> f | s \<Turnstile> EN(EF f))"}
+\end{exercise}
+*}
+(*<*)
+theorem main: "mc f = {s. s \<Turnstile> f}";
+apply(induct_tac f);
+apply(auto simp add:EF_lemma);
+done;
+
+lemma aux: "s \<Turnstile> f = (s : mc f)";
+apply(simp add:main);
+done;
+
+lemma "(s \<Turnstile> EF f) = (s \<Turnstile> f | s \<Turnstile> Neg(AX(Neg(EF f))))";
+apply(simp only:aux);
+apply(simp);
+apply(rule ssubst[OF lfp_Tarski[OF mono_ef]], fast);
+done
+
+end
+(*>*)

--- a/doc-src/TutorialI/CTL/document/CTL.tex	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/CTL/document/CTL.tex	Mon Oct 09 10:18:21 2000 +0200
@@ -188,7 +188,7 @@
 holds. However, we first have to show that such a \isa{t} actually exists! This reasoning
 is embodied in the theorem \isa{someI\isadigit{2}{\isacharunderscore}ex}:
 \begin{isabelle}%
-\ \ \ \ \ {\isasymlbrakk}{\isasymexists}a{\isachardot}\ {\isacharquery}P\ a{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymLongrightarrow}\ {\isacharquery}Q\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}Q\ {\isacharparenleft}Eps\ {\isacharquery}P{\isacharparenright}%
+\ \ \ \ \ {\isasymlbrakk}{\isasymexists}a{\isachardot}\ {\isacharquery}P\ a{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymLongrightarrow}\ {\isacharquery}Q\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}Q\ {\isacharparenleft}SOME\ x{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}%
 \end{isabelle}
 When we apply this theorem as an introduction rule, \isa{{\isacharquery}P\ x} becomes
 \isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ x} and \isa{{\isacharquery}Q\ x} becomes \isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M} and we have to prove
@@ -220,14 +220,15 @@
 \begin{isamarkuptext}%
 Function \isa{path} has fulfilled its purpose now and can be forgotten
 about. It was merely defined to provide the witness in the proof of the
-\isa{infinity{\isacharunderscore}lemma}. Afficionados of minimal proofs might like to know
+\isa{infinity{\isacharunderscore}lemma}. Aficionados of minimal proofs might like to know
 that we could have given the witness without having to define a new function:
 the term
 \begin{isabelle}%
 \ \ \ \ \ nat{\isacharunderscore}rec\ s\ {\isacharparenleft}{\isasymlambda}n\ t{\isachardot}\ SOME\ u{\isachardot}\ {\isacharparenleft}t{\isacharcomma}\ u{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ u{\isacharparenright}%
 \end{isabelle}
+is extensionally equal to \isa{path\ s\ P},
 where \isa{nat{\isacharunderscore}rec} is the predefined primitive recursor on \isa{nat}, whose defining
-equations we omit, is extensionally equal to \isa{path\ s\ P}.%
+equations we omit.%
 \end{isamarkuptext}%
 %
 \begin{isamarkuptext}%
@@ -271,6 +272,22 @@
 \isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ EF{\isacharunderscore}lemma\ equalityI{\isacharbrackleft}OF\ AF{\isacharunderscore}lemma\isadigit{1}\ AF{\isacharunderscore}lemma\isadigit{2}{\isacharbrackright}{\isacharparenright}\isanewline
 \isacommand{done}%
 \begin{isamarkuptext}%
+The above language is not quite CTL. The latter also includes an
+until-operator, usually written as an infix \isa{U}. The formula
+\isa{f\ U\ g} means ``\isa{f} until \isa{g}''.
+It is not definable in terms of the other operators!
+\begin{exercise}
+Extend the datatype of formulae by the until operator with semantics
+\begin{isabelle}%
+\ \ \ \ \ s\ {\isasymTurnstile}\ f\ U\ g\ {\isacharequal}\ {\isacharparenleft}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isacharparenright}%
+\end{isabelle}
+and model checking algorithm
+\begin{isabelle}%
+\ \ \ \ \ mc{\isacharparenleft}f\ U\ g{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isachardot}{\isacharparenright}%
+\end{isabelle}
+Prove that the equivalence between semantics and model checking still holds.
+\end{exercise}
+
 Let us close this section with a few words about the executability of \isa{mc}.
 It is clear that if all sets are finite, they can be represented as lists and the usual
 set operations are easily implemented. Only \isa{lfp} requires a little thought.

--- a/doc-src/TutorialI/CTL/document/PDL.tex	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/CTL/document/PDL.tex	Mon Oct 09 10:18:21 2000 +0200
@@ -173,7 +173,24 @@
 \isacommand{theorem}\ {\isachardoublequote}mc\ f\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ f{\isacharbraceright}{\isachardoublequote}\isanewline
 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline
 \isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}EF{\isacharunderscore}lemma{\isacharparenright}\isanewline
-\isacommand{done}\end{isabellebody}%
+\isacommand{done}%
+\begin{isamarkuptext}%
+\begin{exercise}
+\isa{AX} has a dual operator \isa{EN}\footnote{We cannot use the customary \isa{EX}
+as that is the ASCII equivalent of \isa{{\isasymexists}}}
+(``there exists a next state such that'') with the intended semantics
+\begin{isabelle}%
+\ \ \ \ \ s\ {\isasymTurnstile}\ EN\ f\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymTurnstile}\ f{\isacharparenright}%
+\end{isabelle}
+Fortunately, \isa{EN\ f} can already be expressed as a PDL formula. How?
+
+Show that the semantics for \isa{EF} satisfies the following recursion equation:
+\begin{isabelle}%
+\ \ \ \ \ s\ {\isasymTurnstile}\ EF\ f\ {\isacharequal}\ {\isacharparenleft}s\ {\isasymTurnstile}\ f\ {\isasymor}\ s\ {\isasymTurnstile}\ EN\ {\isacharparenleft}EF\ f{\isacharparenright}{\isacharparenright}%
+\end{isabelle}
+\end{exercise}%
+\end{isamarkuptext}%
+\end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"

--- a/doc-src/TutorialI/CodeGen/CodeGen.thy	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/CodeGen/CodeGen.thy	Mon Oct 09 10:18:21 2000 +0200
@@ -14,7 +14,7 @@
 appropriate function itself.
 *}
 
-types 'v binop = "'v \\<Rightarrow> 'v \\<Rightarrow> 'v";
+types 'v binop = "'v \<Rightarrow> 'v \<Rightarrow> 'v";
 datatype ('a,'v)expr = Cex 'v
                      | Vex 'a
                      | Bex "'v binop"  "('a,'v)expr"  "('a,'v)expr";
@@ -27,7 +27,7 @@
 values is easily defined:
 *}
 
-consts value :: "('a,'v)expr \\<Rightarrow> ('a \\<Rightarrow> 'v) \\<Rightarrow> 'v";
+consts value :: "('a,'v)expr \<Rightarrow> ('a \<Rightarrow> 'v) \<Rightarrow> 'v";
 primrec
 "value (Cex v) env = v"
 "value (Vex a) env = env a"
@@ -53,13 +53,13 @@
 unchanged:
 *}
 
-consts exec :: "('a,'v)instr list \\<Rightarrow> ('a\\<Rightarrow>'v) \\<Rightarrow> 'v 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 (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))))";
+    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 @{term"hd"} and @{term"tl"}
@@ -74,7 +74,7 @@
 definition is pretty much obvious:
 *}
 
-consts comp :: "('a,'v)expr \\<Rightarrow> ('a,'v)instr list";
+consts comp :: "('a,'v)expr \<Rightarrow> ('a,'v)instr list";
 primrec
 "comp (Cex v)       = [Const v]"
 "comp (Vex a)       = [Load a]"
@@ -90,7 +90,7 @@
 This theorem needs to be generalized to
 *}
 
-theorem "\\<forall>vs. exec (comp e) s vs = (value e s) # vs";
+theorem "\<forall>vs. exec (comp e) s vs = (value e s) # vs";
 
 txt{*\noindent
 which is proved by induction on @{term"e"} followed by simplification, once
@@ -99,7 +99,7 @@
 *}
 (*<*)oops;(*>*)
 lemma exec_app[simp]:
-  "\\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"; 
+  "\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"; 
 
 txt{*\noindent
 This requires induction on @{term"xs"} and ordinary simplification for the
@@ -107,8 +107,8 @@
 that contains two @{text"case"}-expressions over instructions. Thus we add
 automatic case splitting as well, which finishes the proof:
 *}
-by(induct_tac xs, simp, simp split: instr.split);
-
+apply(induct_tac xs, simp, simp split: instr.split);
+(*<*)done(*>*)
 text{*\noindent
 Note that because \isaindex{auto} performs simplification, it can
 also be modified in the same way @{text simp} can. Thus the proof can be
@@ -116,10 +116,10 @@
 *}
 (*<*)
 declare exec_app[simp del];
-lemma [simp]: "\\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"; 
+lemma [simp]: "\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"; 
 (*>*)
-by(induct_tac xs, auto split: instr.split);
-
+apply(induct_tac xs, auto split: instr.split);
+(*<*)done(*>*)
 text{*\noindent
 Although this is more compact, it is less clear for the reader of the proof.
 
@@ -129,7 +129,7 @@
 its instance.
 *}
 (*<*)
-theorem "\\<forall>vs. exec (comp e) s vs = (value e s) # vs";
+theorem "\<forall>vs. exec (comp e) s vs = (value e s) # vs";
 by(induct_tac e, auto);
 end
 (*>*)

--- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Mon Oct 09 10:18:21 2000 +0200
@@ -98,14 +98,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}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
+\isacommand{apply}{\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}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ auto\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
+\isacommand{apply}{\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/ABexpr.thy	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Datatype/ABexpr.thy	Mon Oct 09 10:18:21 2000 +0200
@@ -101,7 +101,8 @@
 The resulting 8 goals (one for each constructor) are proved in one fell swoop:
 *}
 
-by simp_all;
+apply simp_all;
+(*<*)done(*>*)
 
 text{*
 In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$,

--- a/doc-src/TutorialI/Datatype/Fundata.thy	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Datatype/Fundata.thy	Mon Oct 09 10:18:21 2000 +0200
@@ -35,7 +35,8 @@
 The following lemma has a canonical proof  *}
 
 lemma "map_bt (g o f) T = map_bt g (map_bt f T)";
-by(induct_tac T, simp_all)
+apply(induct_tac T, simp_all)
+done
 
 text{*\noindent
 %apply(induct_tac T);

--- a/doc-src/TutorialI/Datatype/Nested.thy	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Datatype/Nested.thy	Mon Oct 09 10:18:21 2000 +0200
@@ -12,18 +12,18 @@
 datatype ('a,'b)"term" = Var 'a | App 'b "('a,'b)term list";
 
 text{*\noindent
-Note that we need to quote @{text"term"} on the left to avoid confusion with
-the command \isacommand{term}.
+Note that we need to quote @{text term} on the left to avoid confusion with
+the Isabelle command \isacommand{term}.
 Parameter @{typ"'a"} is the type of variables and @{typ"'b"} the type of
 function symbols.
 A mathematical term like $f(x,g(y))$ becomes @{term"App f [Var x, App g
-  [Var y]]"}, where @{term"f"}, @{term"g"}, @{term"x"}, @{term"y"} are
+  [Var y]]"}, where @{term f}, @{term g}, @{term x}, @{term y} are
 suitable values, e.g.\ numbers or strings.
 
-What complicates the definition of @{text"term"} is the nested occurrence of
-@{text"term"} inside @{text"list"} on the right-hand side. In principle,
+What complicates the definition of @{text term} is the nested occurrence of
+@{text term} inside @{text list} on the right-hand side. In principle,
 nested recursion can be eliminated in favour of mutual recursion by unfolding
-the offending datatypes, here @{text"list"}. The result for @{text"term"}
+the offending datatypes, here @{text list}. The result for @{text term}
 would be something like
 \medskip
 
@@ -33,7 +33,7 @@
 \noindent
 Although we do not recommend this unfolding to the user, it shows how to
 simulate nested recursion by mutual recursion.
-Now we return to the initial definition of @{text"term"} using
+Now we return to the initial definition of @{text term} using
 nested recursion.
 
 Let us define a substitution function on terms. Because terms involve term
@@ -41,8 +41,8 @@
 *}
 
 consts
-subst :: "('a\\<Rightarrow>('a,'b)term) \\<Rightarrow> ('a,'b)term      \\<Rightarrow> ('a,'b)term"
-substs:: "('a\\<Rightarrow>('a,'b)term) \\<Rightarrow> ('a,'b)term list \\<Rightarrow> ('a,'b)term list";
+subst :: "('a\<Rightarrow>('a,'b)term) \<Rightarrow> ('a,'b)term      \<Rightarrow> ('a,'b)term"
+substs:: "('a\<Rightarrow>('a,'b)term) \<Rightarrow> ('a,'b)term list \<Rightarrow> ('a,'b)term list";
 
 primrec
   "subst s (Var x) = s x"
@@ -53,7 +53,8 @@
   "substs s (t # ts) = subst s t # substs s ts";
 
 text{*\noindent
-(Please ignore the label @{thm[source]subst_App} for the moment.)
+Individual equations in a primrec definition may be named as shown for @{thm[source]subst_App}.
+The significance of this device will become apparent below.
 
 Similarly, when proving a statement about terms inductively, we need
 to prove a related statement about term lists simultaneously. For example,
@@ -61,12 +62,13 @@
 strengthened and proved as follows:
 *}
 
-lemma "subst  Var t  = (t ::('a,'b)term)  \\<and>
+lemma "subst  Var t  = (t ::('a,'b)term)  \<and>
         substs Var ts = (ts::('a,'b)term list)";
-by(induct_tac t and ts, simp_all);
+apply(induct_tac t and ts, simp_all);
+done
 
 text{*\noindent
-Note that @{term"Var"} is the identity substitution because by definition it
+Note that @{term Var} is the identity substitution because by definition it
 leaves variables unchanged: @{prop"subst Var (Var x) = Var x"}. Note also
 that the type annotations are necessary because otherwise there is nothing in
 the goal to enforce that both halves of the goal talk about the same type
@@ -82,14 +84,14 @@
 its definition is found in theorem @{thm[source]o_def}).
 \end{exercise}
 \begin{exercise}\label{ex:trev-trev}
-  Define a function @{text"trev"} of type @{typ"('a,'b)term => ('a,'b)term"}
+  Define a function @{term trev} of type @{typ"('a,'b)term => ('a,'b)term"}
 that recursively reverses the order of arguments of all function symbols in a
   term. Prove that @{prop"trev(trev t) = t"}.
 \end{exercise}
 
 The experienced functional programmer may feel that our above definition of
-@{term"subst"} is unnecessarily complicated in that @{term"substs"} is
-completely unnecessary. The @{term"App"}-case can be defined directly as
+@{term subst} is unnecessarily complicated in that @{term substs} is
+completely unnecessary. The @{term App}-case can be defined directly as
 @{term[display]"subst s (App f ts) = App f (map (subst s) ts)"}
 where @{term"map"} is the standard list function such that
 @{text"map f [x1,...,xn] = [f x1,...,f xn]"}. This is true, but Isabelle
@@ -98,7 +100,8 @@
 *}
 
 lemma [simp]: "subst s (App f ts) = App f (map (subst s) ts)"
-by(induct_tac ts, simp_all)
+apply(induct_tac ts, simp_all)
+done
 
 text{*\noindent
 What is more, we can now disable the old defining equation as a
@@ -108,19 +111,19 @@
 declare subst_App [simp del]
 
 text{*\noindent
-The advantage is that now we have replaced @{term"substs"} by
-@{term"map"}, we can profit from the large number of pre-proved lemmas
-about @{term"map"}.  Unfortunately inductive proofs about type
-@{text"term"} are still awkward because they expect a conjunction. One
+The advantage is that now we have replaced @{term substs} by
+@{term map}, we can profit from the large number of pre-proved lemmas
+about @{term map}.  Unfortunately inductive proofs about type
+@{text term} are still awkward because they expect a conjunction. One
 could derive a new induction principle as well (see
 \S\ref{sec:derive-ind}), but turns out to be simpler to define
 functions by \isacommand{recdef} instead of \isacommand{primrec}.
 The details are explained in \S\ref{sec:advanced-recdef} below.
 
 Of course, you may also combine mutual and nested recursion. For example,
-constructor @{text"Sum"} in \S\ref{sec:datatype-mut-rec} could take a list of
-expressions as its argument: @{text"Sum"}~@{typ[quotes]"'a aexp list"}.
+constructor @{text Sum} in \S\ref{sec:datatype-mut-rec} could take a list of
+expressions as its argument: @{text Sum}~@{typ[quotes]"'a aexp list"}.
 *}
 (*<*)
 end
-(*>*)
+(*>*)
\ No newline at end of file

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

--- a/doc-src/TutorialI/Datatype/document/Fundata.tex	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Fundata.tex	Mon Oct 09 10:18:21 2000 +0200
@@ -36,7 +36,8 @@
 The following lemma has a canonical proof%
 \end{isamarkuptext}%
 \isacommand{lemma}\ {\isachardoublequote}map{\isacharunderscore}bt\ {\isacharparenleft}g\ o\ f{\isacharparenright}\ T\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ T{\isacharparenright}{\isachardoublequote}\isanewline
-\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ T{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ T{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
+\isacommand{done}%
 \begin{isamarkuptext}%
 \noindent
 %apply(induct_tac T);

--- a/doc-src/TutorialI/Datatype/document/Nested.tex	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex	Mon Oct 09 10:18:21 2000 +0200
@@ -12,7 +12,7 @@
 \begin{isamarkuptext}%
 \noindent
 Note that we need to quote \isa{term} on the left to avoid confusion with
-the command \isacommand{term}.
+the Isabelle command \isacommand{term}.
 Parameter \isa{{\isacharprime}a} is the type of variables and \isa{{\isacharprime}b} the type of
 function symbols.
 A mathematical term like $f(x,g(y))$ becomes \isa{App\ f\ {\isacharbrackleft}Var\ x{\isacharcomma}\ App\ g\ {\isacharbrackleft}Var\ y{\isacharbrackright}{\isacharbrackright}}, where \isa{f}, \isa{g}, \isa{x}, \isa{y} are
@@ -50,7 +50,8 @@
 \ \ {\isachardoublequote}substs\ s\ {\isacharparenleft}t\ {\isacharhash}\ ts{\isacharparenright}\ {\isacharequal}\ subst\ s\ t\ {\isacharhash}\ substs\ s\ ts{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
-(Please ignore the label \isa{subst{\isacharunderscore}App} for the moment.)
+Individual equations in a primrec definition may be named as shown for \isa{subst{\isacharunderscore}App}.
+The significance of this device will become apparent below.
 
 Similarly, when proving a statement about terms inductively, we need
 to prove a related statement about term lists simultaneously. For example,
@@ -59,7 +60,8 @@
 \end{isamarkuptext}%
 \isacommand{lemma}\ {\isachardoublequote}subst\ \ Var\ t\ \ {\isacharequal}\ {\isacharparenleft}t\ {\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharparenright}\ \ {\isasymand}\isanewline
 \ \ \ \ \ \ \ \ substs\ Var\ ts\ {\isacharequal}\ {\isacharparenleft}ts{\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ list{\isacharparenright}{\isachardoublequote}\isanewline
-\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ \isakeyword{and}\ ts{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ \isakeyword{and}\ ts{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
+\isacommand{done}%
 \begin{isamarkuptext}%
 \noindent
 Note that \isa{Var} is the identity substitution because by definition it
@@ -97,7 +99,8 @@
 that the suggested equation holds:%
 \end{isamarkuptext}%
 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}map\ {\isacharparenleft}subst\ s{\isacharparenright}\ ts{\isacharparenright}{\isachardoublequote}\isanewline
-\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ ts{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ ts{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
+\isacommand{done}%
 \begin{isamarkuptext}%
 \noindent
 What is more, we can now disable the old defining equation as a

--- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Mon Oct 09 10:18:21 2000 +0200
@@ -92,7 +92,8 @@
 *}
 
 apply(induct_tac b);
-by(auto);
+apply(auto);
+done
 
 text{*\noindent
 In fact, all proofs in this case study look exactly like this. Hence we do

--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Mon Oct 09 10:18:21 2000 +0200
@@ -85,7 +85,8 @@
 The proof is canonical:%
 \end{isamarkuptxt}%
 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ b{\isacharparenright}\isanewline
-\isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
+\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline
+\isacommand{done}%
 \begin{isamarkuptext}%
 \noindent
 In fact, all proofs in this case study look exactly like this. Hence we do

--- a/doc-src/TutorialI/Misc/arith1.thy	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Misc/arith1.thy	Mon Oct 09 10:18:21 2000 +0200
@@ -1,7 +1,7 @@
 (*<*)
 theory arith1 = Main:;
 (*>*)
-lemma "\\<lbrakk> \\<not> m < n; m < n+1 \\<rbrakk> \\<Longrightarrow> m = n";
+lemma "\<lbrakk> \<not> m < n; m < n+1 \<rbrakk> \<Longrightarrow> m = n";
 (**)(*<*)
 by(auto);
 end

--- a/doc-src/TutorialI/Misc/arith2.thy	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Misc/arith2.thy	Mon Oct 09 10:18:21 2000 +0200
@@ -2,7 +2,8 @@
 theory arith2 = Main:;
 (*>*)
 lemma "min i (max j (k*k)) = max (min (k*k) i) (min i (j::nat))";
-by(arith);
+apply(arith);
 (**)(*<*)
+done
 end
 (*>*)

--- a/doc-src/TutorialI/Misc/case_exprs.thy	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Misc/case_exprs.thy	Mon Oct 09 10:18:21 2000 +0200
@@ -65,8 +65,8 @@
 which is solved automatically:
 *}
 
-by(auto)
-
+apply(auto)
+(*<*)done(*>*)
 text{*
 Note that we do not need to give a lemma a name if we do not intend to refer
 to it explicitly in the future.

--- a/doc-src/TutorialI/Misc/document/arith2.tex	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/arith2.tex	Mon Oct 09 10:18:21 2000 +0200
@@ -2,7 +2,7 @@
 \begin{isabellebody}%
 \def\isabellecontext{arith2}%
 \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
+\isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline
 \end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex

--- a/doc-src/TutorialI/Misc/document/case_exprs.tex	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/case_exprs.tex	Mon Oct 09 10:18:21 2000 +0200
@@ -71,7 +71,7 @@
 \end{isabelle}
 which is solved automatically:%
 \end{isamarkuptxt}%
-\isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
+\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}%
 \begin{isamarkuptext}%
 Note that we do not need to give a lemma a name if we do not intend to refer
 to it explicitly in the future.%

--- a/doc-src/TutorialI/Misc/document/natsum.tex	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex	Mon Oct 09 10:18:21 2000 +0200
@@ -19,7 +19,8 @@
 \end{isamarkuptext}%
 \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
+\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline
+\isacommand{done}\isanewline
 \end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex

--- a/doc-src/TutorialI/Misc/document/simp.tex	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/simp.tex	Mon Oct 09 10:18:21 2000 +0200
@@ -81,7 +81,8 @@
 as simplification rules and are simplified themselves. For example:%
 \end{isamarkuptext}%
 \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%
+\isacommand{apply}\ simp\isanewline
+\isacommand{done}%
 \begin{isamarkuptext}%
 \noindent
 The second assumption simplifies to \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}, which in turn
@@ -100,7 +101,8 @@
 nontermination but not this one. The problem can be circumvented by
 explicitly telling the simplifier to ignore the assumptions:%
 \end{isamarkuptxt}%
-\isacommand{by}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharparenright}%
+\isacommand{apply}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharparenright}\isanewline
+\isacommand{done}%
 \begin{isamarkuptext}%
 \noindent
 There are three options that influence the treatment of assumptions:
@@ -152,9 +154,9 @@
 \begin{isabelle}
 ~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A%
 \end{isabelle}
-can be proved by simplification. Thus we could have proved the lemma outright%
+can be proved by simplification. Thus we could have proved the lemma outright by%
 \end{isamarkuptxt}%
-\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ exor{\isacharunderscore}def{\isacharparenright}%
+\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ exor{\isacharunderscore}def{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
 Of course we can also unfold definitions in the middle of a proof.
@@ -180,7 +182,8 @@
 \isa{Let{\isacharunderscore}def}:%
 \end{isamarkuptext}%
 \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}%
+\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}\isanewline
+\isacommand{done}%
 \begin{isamarkuptext}%
 If, in a particular context, there is no danger of a combinatorial explosion
 of nested \isa{let}s one could even simlify with \isa{Let{\isacharunderscore}def} by
@@ -194,7 +197,8 @@
 accepts \emph{conditional} equations, for example%
 \end{isamarkuptext}%
 \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}%
+\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp{\isacharparenright}\isanewline
+\isacommand{done}%
 \begin{isamarkuptext}%
 \noindent
 Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a
@@ -259,7 +263,7 @@
 in case of recursive datatypes. Again, if the \isa{only{\isacharcolon}} modifier is
 dropped, the above goal is solved,%
 \end{isamarkuptext}%
-\isacommand{by}{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}%
+\isacommand{apply}{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent%
 which \isacommand{apply}\isa{{\isacharparenleft}simp{\isacharparenright}} alone will not do.

--- a/doc-src/TutorialI/Misc/natsum.thy	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Misc/natsum.thy	Mon Oct 09 10:18:21 2000 +0200
@@ -17,7 +17,8 @@
 
 lemma "sum n + sum n = n*(Suc n)";
 apply(induct_tac n);
-by(auto);
+apply(auto);
+done
 
 (*<*)
 end

--- a/doc-src/TutorialI/Misc/simp.thy	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Misc/simp.thy	Mon Oct 09 10:18:21 2000 +0200
@@ -79,8 +79,9 @@
 as simplification rules and are simplified themselves. For example:
 *}
 
-lemma "\\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \\<rbrakk> \\<Longrightarrow> ys = zs";
-by simp;
+lemma "\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \<rbrakk> \<Longrightarrow> ys = zs";
+apply simp;
+done
 
 text{*\noindent
 The second assumption simplifies to @{term"xs = []"}, which in turn
@@ -91,7 +92,7 @@
 nontermination:
 *}
 
-lemma "\\<forall>x. f x = g (f (g x)) \\<Longrightarrow> f [] = f [] @ []";
+lemma "\<forall>x. f x = g (f (g x)) \<Longrightarrow> f [] = f [] @ []";
 
 txt{*\noindent
 cannot be solved by an unmodified application of @{text"simp"} because the
@@ -101,7 +102,8 @@
 explicitly telling the simplifier to ignore the assumptions:
 *}
 
-by(simp (no_asm));
+apply(simp (no_asm));
+done
 
 text{*\noindent
 There are three options that influence the treatment of assumptions:
@@ -134,14 +136,14 @@
 original definition. For example, given
 *}
 
-constdefs exor :: "bool \\<Rightarrow> bool \\<Rightarrow> bool"
-         "exor A B \\<equiv> (A \\<and> \\<not>B) \\<or> (\\<not>A \\<and> B)";
+constdefs exor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
+         "exor A B \<equiv> (A \<and> \<not>B) \<or> (\<not>A \<and> B)";
 
 text{*\noindent
 we may want to prove
 *}
 
-lemma "exor A (\\<not>A)";
+lemma "exor A (\<not>A)";
 
 txt{*\noindent
 Typically, the opening move consists in \emph{unfolding} the definition(s), which we need to
@@ -155,10 +157,10 @@
 \begin{isabelle}
 ~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A%
 \end{isabelle}
-can be proved by simplification. Thus we could have proved the lemma outright
-*}(*<*)oops;lemma "exor A (\\<not>A)";(*>*)
-by(simp add: exor_def)
-
+can be proved by simplification. Thus we could have proved the lemma outright by
+*}(*<*)oops;lemma "exor A (\<not>A)";(*>*)
+apply(simp add: exor_def)
+(*<*)done(*>*)
 text{*\noindent
 Of course we can also unfold definitions in the middle of a proof.
 
@@ -183,7 +185,8 @@
 *}
 
 lemma "(let xs = [] in xs@ys@xs) = ys";
-by(simp add: Let_def);
+apply(simp add: Let_def);
+done
 
 text{*
 If, in a particular context, there is no danger of a combinatorial explosion
@@ -199,8 +202,9 @@
 accepts \emph{conditional} equations, for example
 *}
 
-lemma hd_Cons_tl[simp]: "xs \\<noteq> []  \\<Longrightarrow>  hd xs # tl xs = xs";
-by(case_tac xs, simp, simp);
+lemma hd_Cons_tl[simp]: "xs \<noteq> []  \<Longrightarrow>  hd xs # tl xs = xs";
+apply(case_tac xs, simp, simp);
+done
 
 text{*\noindent
 Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a
@@ -209,7 +213,7 @@
 is present as well,
 *}
 
-lemma "xs \\<noteq> [] \\<Longrightarrow> hd(rev xs) # tl(rev xs) = rev xs";
+lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) # tl(rev xs) = rev xs";
 (*<*)
 by(simp);
 (*>*)
@@ -230,7 +234,7 @@
 distinction on the condition of the @{text"if"}. For example the goal
 *}
 
-lemma "\\<forall>xs. if xs = [] then rev xs = [] else rev xs \\<noteq> []";
+lemma "\<forall>xs. if xs = [] then rev xs = [] else rev xs \<noteq> []";
 
 txt{*\noindent
 can be split into
@@ -254,7 +258,7 @@
 This splitting idea generalizes from @{text"if"} to \isaindex{case}:
 *}
 
-lemma "(case xs of [] \\<Rightarrow> zs | y#ys \\<Rightarrow> y#(ys@zs)) = xs@zs";
+lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs";
 txt{*\noindent
 becomes
 \begin{isabelle}\makeatother
@@ -274,10 +278,10 @@
 dropped, the above goal is solved,
 *}
 (*<*)
-lemma "(case xs of [] \\<Rightarrow> zs | y#ys \\<Rightarrow> y#(ys@zs)) = xs@zs";
+lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs";
 (*>*)
-by(simp split: list.split);
-
+apply(simp split: list.split);
+(*<*)done(*>*)
 text{*\noindent%
 which \isacommand{apply}@{text"(simp)"} alone will not do.
 
@@ -350,14 +354,14 @@
 (@{text"="}, \isasymle, @{text"<"}) and it only knows about addition. Thus
 *}
 
-lemma "\\<lbrakk> \\<not> m < n; m < n+1 \\<rbrakk> \\<Longrightarrow> m = n"
+lemma "\<lbrakk> \<not> m < n; m < n+1 \<rbrakk> \<Longrightarrow> m = n"
 (*<*)by(auto)(*>*)
 
 text{*\noindent
 is proved by simplification, whereas the only slightly more complex
 *}
 
-lemma "\\<not> m < n \\<and> m < n+1 \\<Longrightarrow> m = n";
+lemma "\<not> m < n \<and> m < n+1 \<Longrightarrow> m = n";
 (*<*)by(arith)(*>*)
 
 text{*\noindent

--- a/doc-src/TutorialI/Recdef/Induction.thy	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Induction.thy	Mon Oct 09 10:18:21 2000 +0200
@@ -41,7 +41,8 @@
 The rest is pure simplification:
 *}
 
-by simp_all;
+apply simp_all;
+done
 
 text{*
 Try proving the above lemma by structural induction, and you find that you

--- a/doc-src/TutorialI/Recdef/Nested1.thy	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Nested1.thy	Mon Oct 09 10:18:21 2000 +0200
@@ -4,12 +4,12 @@
 consts trev  :: "('a,'b)term \<Rightarrow> ('a,'b)term";
 
 text{*\noindent
-Although the definition of @{term"trev"} is quite natural, we will have
+Although the definition of @{term trev} is quite natural, we will have
 overcome a minor difficulty in convincing Isabelle of is termination.
 It is precisely this difficulty that is the \textit{raison d'\^etre} of
 this subsection.
 
-Defining @{term"trev"} by \isacommand{recdef} rather than \isacommand{primrec}
+Defining @{term trev} by \isacommand{recdef} rather than \isacommand{primrec}
 simplifies matters because we are now free to use the recursion equation
 suggested at the end of \S\ref{sec:nested-datatype}:
 *};
@@ -19,22 +19,22 @@
  "trev (App f ts) = App f (rev(map trev ts))";
 
 text{*\noindent
-Remember that function @{term"size"} is defined for each \isacommand{datatype}.
+Remember that function @{term size} is defined for each \isacommand{datatype}.
 However, the definition does not succeed. Isabelle complains about an
 unproved termination condition
 @{term[display]"t : set ts --> size t < Suc (term_list_size ts)"}
-where @{term"set"} returns the set of elements of a list
+where @{term set} returns the set of elements of a list
 and @{text"term_list_size :: term list \<Rightarrow> nat"} is an auxiliary
 function automatically defined by Isabelle
-(when @{text"term"} was defined).  First we have to understand why the
-recursive call of @{term"trev"} underneath @{term"map"} leads to the above
-condition. The reason is that \isacommand{recdef} ``knows'' that @{term"map"}
-will apply @{term"trev"} only to elements of @{term"ts"}. Thus the above
-condition expresses that the size of the argument @{term"t : set ts"} of any
-recursive call of @{term"trev"} is strictly less than @{term"size(App f ts) =
+(when @{text term} was defined).  First we have to understand why the
+recursive call of @{term trev} underneath @{term map} leads to the above
+condition. The reason is that \isacommand{recdef} ``knows'' that @{term map}
+will apply @{term trev} only to elements of @{term ts}. Thus the above
+condition expresses that the size of the argument @{prop"t : set ts"} of any
+recursive call of @{term trev} is strictly less than @{prop"size(App f ts) =
 Suc(term_list_size ts)"}.  We will now prove the termination condition and
 continue with our definition.  Below we return to the question of how
-\isacommand{recdef} ``knows'' about @{term"map"}.
+\isacommand{recdef} ``knows'' about @{term map}.
 *};
 
 (*<*)

--- a/doc-src/TutorialI/Recdef/Nested2.thy	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Nested2.thy	Mon Oct 09 10:18:21 2000 +0200
@@ -78,7 +78,7 @@
 recdef dummy "{}"
 "dummy n = n"
 (*>*)
-(hints cong: map_cong)
+(hints recdef_cong: map_cong)
 
 text{*\noindent
 or declare them globally
@@ -88,11 +88,11 @@
 declare map_cong[recdef_cong];
 
 text{*
-Note that the global @{text cong} and @{text recdef_cong} attributes are
+Note that the @{text cong} and @{text recdef_cong} attributes are
 intentionally kept apart because they control different activities, namely
-simplification and making recursive definitions. The local @{text cong} in
-the hints section of \isacommand{recdef} is merely short for @{text
-recdef_cong}.
+simplification and making recursive definitions.
+% The local @{text cong} in
+% the hints section of \isacommand{recdef} is merely short for @{text recdef_cong}.
 %The simplifier's congruence rules cannot be used by recdef.
 %For example the weak congruence rules for if and case would prevent
 %recdef from generating sensible termination conditions.

--- a/doc-src/TutorialI/Recdef/document/Induction.tex	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Induction.tex	Mon Oct 09 10:18:21 2000 +0200
@@ -38,7 +38,8 @@
 \end{isabelle}
 The rest is pure simplification:%
 \end{isamarkuptxt}%
-\isacommand{by}\ simp{\isacharunderscore}all%
+\isacommand{apply}\ simp{\isacharunderscore}all\isanewline
+\isacommand{done}%
 \begin{isamarkuptext}%
 Try proving the above lemma by structural induction, and you find that you
 need an additional case distinction. What is worse, the names of variables

--- a/doc-src/TutorialI/Recdef/document/Nested2.tex	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested2.tex	Mon Oct 09 10:18:21 2000 +0200
@@ -72,7 +72,7 @@
 rules, you can either append a hint locally
 to the specific occurrence of \isacommand{recdef}%
 \end{isamarkuptext}%
-{\isacharparenleft}\isakeyword{hints}\ cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}%
+{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
 or declare them globally
@@ -80,10 +80,11 @@
 \end{isamarkuptext}%
 \isacommand{declare}\ map{\isacharunderscore}cong{\isacharbrackleft}recdef{\isacharunderscore}cong{\isacharbrackright}%
 \begin{isamarkuptext}%
-Note that the global \isa{cong} and \isa{recdef{\isacharunderscore}cong} attributes are
+Note that the \isa{cong} and \isa{recdef{\isacharunderscore}cong} attributes are
 intentionally kept apart because they control different activities, namely
-simplification and making recursive definitions. The local \isa{cong} in
-the hints section of \isacommand{recdef} is merely short for \isa{recdef{\isacharunderscore}cong}.
+simplification and making recursive definitions.
+% The local \isa{cong} in
+% the hints section of \isacommand{recdef} is merely short for \isa{recdef{\isacharunderscore}cong}.
 %The simplifier's congruence rules cannot be used by recdef.
 %For example the weak congruence rules for if and case would prevent
 %recdef from generating sensible termination conditions.%

--- a/doc-src/TutorialI/Recdef/document/simplification.tex	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex	Mon Oct 09 10:18:21 2000 +0200
@@ -23,7 +23,7 @@
 is provded automatically because it is already present as a lemma in the
 arithmetic library. Thus the recursion equation becomes a simplification
 rule. Of course the equation is nonterminating if we are allowed to unfold
-the recursive call inside the \isa{if} branch, which is why programming
+the recursive call inside the \isa{else} branch, which is why programming
 languages and our simplifier don't do that. Unfortunately the simplifier does
 something else which leads to the same problem: it splits \isa{if}s if the
 condition simplifies to neither \isa{True} nor \isa{False}. For
@@ -78,9 +78,11 @@
 derived conditional ones. For \isa{gcd} it means we have to prove%
 \end{isamarkuptext}%
 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}gcd\ {\isacharparenleft}m{\isacharcomma}\ \isadigit{0}{\isacharparenright}\ {\isacharequal}\ m{\isachardoublequote}\isanewline
-\isacommand{by}{\isacharparenleft}simp{\isacharparenright}\isanewline
+\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
+\isacommand{done}\isanewline
 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}n\ {\isasymnoteq}\ \isadigit{0}\ {\isasymLongrightarrow}\ gcd{\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ gcd{\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isachardoublequote}\isanewline
-\isacommand{by}{\isacharparenleft}simp{\isacharparenright}%
+\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
+\isacommand{done}%
 \begin{isamarkuptext}%
 \noindent
 after which we can disable the original simplification rule:%

--- a/doc-src/TutorialI/Recdef/document/termination.tex	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/termination.tex	Mon Oct 09 10:18:21 2000 +0200
@@ -33,7 +33,8 @@
 It was not proved automatically because of the special nature of \isa{{\isacharminus}}
 on \isa{nat}. This requires more arithmetic than is tried by default:%
 \end{isamarkuptxt}%
-\isacommand{by}{\isacharparenleft}arith{\isacharparenright}%
+\isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline
+\isacommand{done}%
 \begin{isamarkuptext}%
 \noindent
 Because \isacommand{recdef}'s termination prover involves simplification,
@@ -51,7 +52,8 @@
 rules. Thus we can automatically prove%
 \end{isamarkuptext}%
 \isacommand{theorem}\ {\isachardoublequote}g{\isacharparenleft}\isadigit{1}{\isacharcomma}\isadigit{0}{\isacharparenright}\ {\isacharequal}\ g{\isacharparenleft}\isadigit{1}{\isacharcomma}\isadigit{1}{\isacharparenright}{\isachardoublequote}\isanewline
-\isacommand{by}{\isacharparenleft}simp{\isacharparenright}%
+\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
+\isacommand{done}%
 \begin{isamarkuptext}%
 \noindent
 More exciting theorems require induction, which is discussed below.

--- a/doc-src/TutorialI/Recdef/simplification.thy	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Recdef/simplification.thy	Mon Oct 09 10:18:21 2000 +0200
@@ -7,12 +7,12 @@
 equations become simplification rules, just as with
 \isacommand{primrec}. In most cases this works fine, but there is a subtle
 problem that must be mentioned: simplification may not
-terminate because of automatic splitting of @{text"if"}.
+terminate because of automatic splitting of @{text if}.
 Let us look at an example:
 *}
 
-consts gcd :: "nat\<times>nat \\<Rightarrow> nat";
-recdef gcd "measure (\\<lambda>(m,n).n)"
+consts gcd :: "nat\<times>nat \<Rightarrow> nat";
+recdef gcd "measure (\<lambda>(m,n).n)"
   "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))";
 
 text{*\noindent
@@ -22,10 +22,10 @@
 is provded automatically because it is already present as a lemma in the
 arithmetic library. Thus the recursion equation becomes a simplification
 rule. Of course the equation is nonterminating if we are allowed to unfold
-the recursive call inside the @{text"if"} branch, which is why programming
+the recursive call inside the @{text else} branch, which is why programming
 languages and our simplifier don't do that. Unfortunately the simplifier does
-something else which leads to the same problem: it splits @{text"if"}s if the
-condition simplifies to neither @{term"True"} nor @{term"False"}. For
+something else which leads to the same problem: it splits @{text if}s if the
+condition simplifies to neither @{term True} nor @{term False}. For
 example, simplification reduces
 @{term[display]"gcd(m,n) = k"}
 in one step to
@@ -33,23 +33,23 @@
 where the condition cannot be reduced further, and splitting leads to
 @{term[display]"(n=0 --> m=k) & (n ~= 0 --> gcd(n, m mod n)=k)"}
 Since the recursive call @{term"gcd(n, m mod n)"} is no longer protected by
-an @{text"if"}, it is unfolded again, which leads to an infinite chain of
+an @{text if}, it is unfolded again, which leads to an infinite chain of
 simplification steps. Fortunately, this problem can be avoided in many
 different ways.
 
 The most radical solution is to disable the offending
 @{thm[source]split_if} as shown in the section on case splits in
 \S\ref{sec:Simplification}.  However, we do not recommend this because it
-means you will often have to invoke the rule explicitly when @{text"if"} is
+means you will often have to invoke the rule explicitly when @{text if} is
 involved.
 
 If possible, the definition should be given by pattern matching on the left
-rather than @{text"if"} on the right. In the case of @{term"gcd"} the
+rather than @{text if} on the right. In the case of @{term gcd} the
 following alternative definition suggests itself:
 *}
 
-consts gcd1 :: "nat\<times>nat \\<Rightarrow> nat";
-recdef gcd1 "measure (\\<lambda>(m,n).n)"
+consts gcd1 :: "nat\<times>nat \<Rightarrow> nat";
+recdef gcd1 "measure (\<lambda>(m,n).n)"
   "gcd1 (m, 0) = m"
   "gcd1 (m, n) = gcd1(n, m mod n)";
 
@@ -59,25 +59,27 @@
 @{prop"n ~= 0"}. Unfortunately, in general the case distinction
 may not be expressible by pattern matching.
 
-A very simple alternative is to replace @{text"if"} by @{text"case"}, which
+A very simple alternative is to replace @{text if} by @{text case}, which
 is also available for @{typ"bool"} but is not split automatically:
 *}
 
-consts gcd2 :: "nat\<times>nat \\<Rightarrow> nat";
-recdef gcd2 "measure (\\<lambda>(m,n).n)"
-  "gcd2(m,n) = (case n=0 of True \\<Rightarrow> m | False \\<Rightarrow> gcd2(n,m mod n))";
+consts gcd2 :: "nat\<times>nat \<Rightarrow> nat";
+recdef gcd2 "measure (\<lambda>(m,n).n)"
+  "gcd2(m,n) = (case n=0 of True \<Rightarrow> m | False \<Rightarrow> gcd2(n,m mod n))";
 
 text{*\noindent
 In fact, this is probably the neatest solution next to pattern matching.
 
 A final alternative is to replace the offending simplification rules by
-derived conditional ones. For @{term"gcd"} it means we have to prove
+derived conditional ones. For @{term gcd} it means we have to prove
 *}
 
 lemma [simp]: "gcd (m, 0) = m";
-by(simp);
-lemma [simp]: "n \\<noteq> 0 \\<Longrightarrow> gcd(m, n) = gcd(n, m mod n)";
-by(simp);
+apply(simp);
+done
+lemma [simp]: "n \<noteq> 0 \<Longrightarrow> gcd(m, n) = gcd(n, m mod n)";
+apply(simp);
+done
 
 text{*\noindent
 after which we can disable the original simplification rule:

--- a/doc-src/TutorialI/Recdef/termination.thy	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Recdef/termination.thy	Mon Oct 09 10:18:21 2000 +0200
@@ -36,7 +36,8 @@
 on @{typ"nat"}. This requires more arithmetic than is tried by default:
 *}
 
-by(arith);
+apply(arith);
+done
 
 text{*\noindent
 Because \isacommand{recdef}'s termination prover involves simplification,
@@ -51,12 +52,13 @@
 
 text{*\noindent
 This time everything works fine. Now @{thm[source]g.simps} contains precisely
-the stated recursion equation for @{term"g"} and they are simplification
+the stated recursion equation for @{term g} and they are simplification
 rules. Thus we can automatically prove
 *}
 
 theorem "g(1,0) = g(1,1)";
-by(simp);
+apply(simp);
+done
 
 text{*\noindent
 More exciting theorems require induction, which is discussed below.
@@ -66,17 +68,17 @@
 \isacommand{hint} is not necessary. But our @{thm[source]termi_lem} is not
 sufficiently general to warrant this distinction.
 
-The attentive reader may wonder why we chose to call our function @{term"g"}
-rather than @{term"f"} the second time around. The reason is that, despite
-the failed termination proof, the definition of @{term"f"} did not
+The attentive reader may wonder why we chose to call our function @{term g}
+rather than @{term f} the second time around. The reason is that, despite
+the failed termination proof, the definition of @{term f} did not
 fail, and thus we could not define it a second time. However, all theorems
-about @{term"f"}, for example @{thm[source]f.simps}, carry as a precondition
+about @{term f}, for example @{thm[source]f.simps}, carry as a precondition
 the unproved termination condition. Moreover, the theorems
 @{thm[source]f.simps} are not simplification rules. However, this mechanism
 allows a delayed proof of termination: instead of proving
 @{thm[source]termi_lem} up front, we could prove 
 it later on and then use it to remove the preconditions from the theorems
-about @{term"f"}. In most cases this is more cumbersome than proving things
+about @{term f}. In most cases this is more cumbersome than proving things
 up front.
 %FIXME, with one exception: nested recursion.
 

--- a/doc-src/TutorialI/ToyList/ToyList.thy	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/ToyList/ToyList.thy	Mon Oct 09 10:18:21 2000 +0200
@@ -281,14 +281,17 @@
 We still need to confirm that the proof is now finished:
 *}
 
-.
+done
 
-text{*\noindent\indexbold{$Isar@\texttt{.}}%
-As a result of that final dot, Isabelle associates the lemma
-just proved with its name. Instead of \isacommand{apply}
-followed by a dot, you can simply write \isacommand{by}\indexbold{by},
-which we do most of the time. Notice that in lemma @{thm[source]app_Nil2}
-(as printed out after the final dot) the free variable @{term"xs"} has been
+text{*\noindent\indexbold{done}%
+As a result of that final \isacommand{done}, Isabelle associates the lemma just proved
+with its name. In this tutorial, we sometimes omit to show that final \isacommand{done}
+if it is obvious from the context that the proof is finished.
+
+% Instead of \isacommand{apply} followed by a dot, you can simply write
+% \isacommand{by}\indexbold{by}, which we do most of the time.
+Notice that in lemma @{thm[source]app_Nil2}
+(as printed out after the final \isacommand{done}) the free variable @{term"xs"} has been
 replaced by the unknown @{text"?xs"}, just as explained in
 \S\ref{sec:variables}.
 
@@ -326,7 +329,8 @@
 
 lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)";
 apply(induct_tac xs);
-by(auto);
+apply(auto);
+done
 
 text{*
 \noindent
@@ -336,7 +340,8 @@
 
 lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
 apply(induct_tac xs);
-by(auto);
+apply(auto);
+done
 
 text{*\noindent
 and then solve our main theorem:
@@ -344,7 +349,8 @@
 
 theorem rev_rev [simp]: "rev(rev xs) = xs";
 apply(induct_tac xs);
-by(auto);
+apply(auto);
+done
 
 text{*\noindent
 The final \isacommand{end} tells Isabelle to close the current theory because

--- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Mon Oct 09 10:18:21 2000 +0200
@@ -261,14 +261,17 @@
 
 We still need to confirm that the proof is now finished:%
 \end{isamarkuptxt}%
-\isacommand{{\isachardot}}%
+\isacommand{done}%
 \begin{isamarkuptext}%
-\noindent\indexbold{$Isar@\texttt{.}}%
-As a result of that final dot, Isabelle associates the lemma
-just proved with its name. Instead of \isacommand{apply}
-followed by a dot, you can simply write \isacommand{by}\indexbold{by},
-which we do most of the time. Notice that in lemma \isa{app{\isacharunderscore}Nil\isadigit{2}}
-(as printed out after the final dot) the free variable \isa{xs} has been
+\noindent\indexbold{done}%
+As a result of that final \isacommand{done}, Isabelle associates the lemma just proved
+with its name. In this tutorial, we sometimes omit to show that final \isacommand{done}
+if it is obvious from the context that the proof is finished.
+
+% Instead of \isacommand{apply} followed by a dot, you can simply write
+% \isacommand{by}\indexbold{by}, which we do most of the time.
+Notice that in lemma \isa{app{\isacharunderscore}Nil\isadigit{2}}
+(as printed out after the final \isacommand{done}) the free variable \isa{xs} has been
 replaced by the unknown \isa{{\isacharquery}xs}, just as explained in
 \S\ref{sec:variables}.
 
@@ -302,7 +305,8 @@
 \end{isamarkuptext}%
 \isacommand{lemma}\ app{\isacharunderscore}assoc\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}{\isachardoublequote}\isanewline
 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
-\isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
+\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline
+\isacommand{done}%
 \begin{isamarkuptext}%
 \noindent
 succeeds without further ado.
@@ -310,14 +314,16 @@
 \end{isamarkuptext}%
 \isacommand{lemma}\ rev{\isacharunderscore}app\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequote}\isanewline
 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
-\isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
+\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline
+\isacommand{done}%
 \begin{isamarkuptext}%
 \noindent
 and then solve our main theorem:%
 \end{isamarkuptext}%
 \isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
-\isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
+\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline
+\isacommand{done}%
 \begin{isamarkuptext}%
 \noindent
 The final \isacommand{end} tells Isabelle to close the current theory because

--- a/doc-src/TutorialI/ToyList2/ToyList2	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/ToyList2/ToyList2	Mon Oct 09 10:18:21 2000 +0200
@@ -1,18 +1,21 @@
 lemma app_Nil2 [simp]: "xs @ [] = xs"
 apply(induct_tac xs)
 apply(auto)
-.
+done
 
 lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
 apply(induct_tac xs)
-by(auto)
+apply(auto)
+done
 
 lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"
 apply(induct_tac xs)
-by(auto)
+apply(auto)
+done
 
 theorem rev_rev [simp]: "rev(rev xs) = xs"
 apply(induct_tac xs)
-by(auto)
+apply(auto)
+done
 
 end

--- a/doc-src/TutorialI/Trie/Trie.thy	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Trie/Trie.thy	Mon Oct 09 10:18:21 2000 +0200
@@ -18,8 +18,8 @@
 We define two selector functions:
 *};
 
-consts value :: "('a,'v)trie \\<Rightarrow> 'v option"
-       alist :: "('a,'v)trie \\<Rightarrow> ('a * ('a,'v)trie)list";
+consts value :: "('a,'v)trie \<Rightarrow> 'v option"
+       alist :: "('a,'v)trie \<Rightarrow> ('a * ('a,'v)trie)list";
 primrec "value(Trie ov al) = ov";
 primrec "alist(Trie ov al) = al";
 
@@ -27,7 +27,7 @@
 Association lists come with a generic lookup function:
 *};
 
-consts   assoc :: "('key * 'val)list \\<Rightarrow> 'key \\<Rightarrow> 'val option";
+consts   assoc :: "('key * 'val)list \<Rightarrow> 'key \<Rightarrow> 'val option";
 primrec "assoc [] x = None"
         "assoc (p#ps) x =
            (let (a,b) = p in if a=x then Some b else assoc ps x)";
@@ -39,20 +39,21 @@
 recursion on the search string argument:
 *};
 
-consts   lookup :: "('a,'v)trie \\<Rightarrow> 'a list \\<Rightarrow> 'v option";
+consts   lookup :: "('a,'v)trie \<Rightarrow> 'a list \<Rightarrow> 'v option";
 primrec "lookup t [] = value t"
         "lookup t (a#as) = (case assoc (alist t) a of
-                              None \\<Rightarrow> None
-                            | Some at \\<Rightarrow> lookup at as)";
+                              None \<Rightarrow> None
+                            | Some at \<Rightarrow> lookup at as)";
 
 text{*
 As a first simple property we prove that looking up a string in the empty
-trie @{term"Trie None []"} always returns @{term"None"}. The proof merely
+trie @{term"Trie None []"} always returns @{term None}. The proof merely
 distinguishes the two cases whether the search string is empty or not:
 *};
 
 lemma [simp]: "lookup (Trie None []) as = None";
-by(case_tac as, simp_all);
+apply(case_tac as, simp_all);
+done
 
 text{*
 Things begin to get interesting with the definition of an update function
@@ -60,24 +61,24 @@
 associated with that string:
 *};
 
-consts update :: "('a,'v)trie \\<Rightarrow> 'a list \\<Rightarrow> 'v \\<Rightarrow> ('a,'v)trie";
+consts update :: "('a,'v)trie \<Rightarrow> 'a list \<Rightarrow> 'v \<Rightarrow> ('a,'v)trie";
 primrec
   "update t []     v = Trie (Some v) (alist t)"
   "update t (a#as) v =
      (let tt = (case assoc (alist t) a of
-                  None \\<Rightarrow> Trie None [] | Some at \\<Rightarrow> at)
+                  None \<Rightarrow> Trie None [] | Some at \<Rightarrow> at)
       in Trie (value t) ((a,update tt as v)#alist t))";
 
 text{*\noindent
 The base case is obvious. In the recursive case the subtrie
-@{term"tt"} associated with the first letter @{term"a"} is extracted,
+@{term tt} associated with the first letter @{term a} is extracted,
 recursively updated, and then placed in front of the association list.
-The old subtrie associated with @{term"a"} is still in the association list
-but no longer accessible via @{term"assoc"}. Clearly, there is room here for
+The old subtrie associated with @{term a} is still in the association list
+but no longer accessible via @{term assoc}. Clearly, there is room here for
 optimizations!
 
-Before we start on any proofs about @{term"update"} we tell the simplifier to
-expand all @{text"let"}s and to split all @{text"case"}-constructs over
+Before we start on any proofs about @{term update} we tell the simplifier to
+expand all @{text let}s and to split all @{text case}-constructs over
 options:
 *};
 
@@ -85,23 +86,23 @@
 
 text{*\noindent
 The reason becomes clear when looking (probably after a failed proof
-attempt) at the body of @{term"update"}: it contains both
-@{text"let"} and a case distinction over type @{text"option"}.
+attempt) at the body of @{term update}: it contains both
+@{text let} and a case distinction over type @{text option}.
 
-Our main goal is to prove the correct interaction of @{term"update"} and
-@{term"lookup"}:
+Our main goal is to prove the correct interaction of @{term update} and
+@{term lookup}:
 *};
 
-theorem "\\<forall>t v bs. lookup (update t as v) bs =
+theorem "\<forall>t v bs. lookup (update t as v) bs =
                     (if as=bs then Some v else lookup t bs)";
 
 txt{*\noindent
-Our plan is to induct on @{term"as"}; hence the remaining variables are
+Our plan is to induct on @{term as}; hence the remaining variables are
 quantified. From the definitions it is clear that induction on either
-@{term"as"} or @{term"bs"} is required. The choice of @{term"as"} is merely
-guided by the intuition that simplification of @{term"lookup"} might be easier
-if @{term"update"} has already been simplified, which can only happen if
-@{term"as"} is instantiated.
+@{term as} or @{term bs} is required. The choice of @{term as} is merely
+guided by the intuition that simplification of @{term lookup} might be easier
+if @{term update} has already been simplified, which can only happen if
+@{term as} is instantiated.
 The start of the proof is completely conventional:
 *};
 apply(induct_tac as, auto);
@@ -113,14 +114,15 @@
 ~2.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline
 ~3.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs
 \end{isabelle}
-Clearly, if we want to make headway we have to instantiate @{term"bs"} as
+Clearly, if we want to make headway we have to instantiate @{term bs} as
 well now. It turns out that instead of induction, case distinction
 suffices:
 *};
-by(case_tac[!] bs, auto);
+apply(case_tac[!] bs, auto);
+done
 
 text{*\noindent
-All methods ending in @{text"tac"} take an optional first argument that
+All methods ending in @{text tac} take an optional first argument that
 specifies the range of subgoals they are applied to, where @{text"[!]"} means
 all subgoals, i.e.\ @{text"[1-3]"} in our case. Individual subgoal numbers,
 e.g. @{text"[2]"} are also allowed.
@@ -128,8 +130,8 @@
 This proof may look surprisingly straightforward. However, note that this
 comes at a cost: the proof script is unreadable because the intermediate
 proof states are invisible, and we rely on the (possibly brittle) magic of
-@{text"auto"} (@{text"simp_all"} will not do---try it) to split the subgoals
-of the induction up in such a way that case distinction on @{term"bs"} makes
+@{text auto} (@{text simp_all} will not do---try it) to split the subgoals
+of the induction up in such a way that case distinction on @{term bs} makes
 sense and solves the proof. Part~\ref{Isar} shows you how to write readable
 and stable proofs.
 *};

--- a/doc-src/TutorialI/Trie/document/Trie.tex	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Trie/document/Trie.tex	Mon Oct 09 10:18:21 2000 +0200
@@ -46,7 +46,8 @@
 distinguishes the two cases whether the search string is empty or not:%
 \end{isamarkuptext}%
 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}lookup\ {\isacharparenleft}Trie\ None\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ as\ {\isacharequal}\ None{\isachardoublequote}\isanewline
-\isacommand{by}{\isacharparenleft}case{\isacharunderscore}tac\ as{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
+\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ as{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
+\isacommand{done}%
 \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
@@ -107,7 +108,8 @@
 well now. It turns out that instead of induction, case distinction
 suffices:%
 \end{isamarkuptxt}%
-\isacommand{by}{\isacharparenleft}case{\isacharunderscore}tac{\isacharbrackleft}{\isacharbang}{\isacharbrackright}\ bs{\isacharcomma}\ auto{\isacharparenright}%
+\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac{\isacharbrackleft}{\isacharbang}{\isacharbrackright}\ bs{\isacharcomma}\ auto{\isacharparenright}\isanewline
+\isacommand{done}%
 \begin{isamarkuptext}%
 \noindent
 All methods ending in \isa{tac} take an optional first argument that

--- a/doc-src/TutorialI/appendix.tex	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/appendix.tex	Mon Oct 09 10:18:21 2000 +0200
@@ -5,80 +5,90 @@
 
 \begin{figure}[htbp]
 \begin{center}
-\begin{tabular}{|ccccccccccc|}
+\begin{tabular}{|l|l|l|}
 \hline
-\indexboldpos{\isasymand}{$HOL0and} &
-\indexboldpos{\isasymor}{$HOL0or} &
-\indexboldpos{\isasymimp}{$HOL0imp} &
-\indexboldpos{\isasymnot}{$HOL0not} &
-\indexboldpos{\isasymnoteq}{$HOL0noteq} &
-\indexboldpos{\isasymforall}{$HOL0All} &
-\isasymforall &
-\indexboldpos{\isasymexists}{$HOL0Ex} &
-\isasymexists &
-\isasymuniqex\index{$HOL0ExU@\isasymuniqex|bold} &
-\isasymuniqex \\
-\texttt{\&}\indexbold{$HOL0and@{\texttt{\&}}} &
-\texttt{|}\index{$HOL0or@\ttor|bold} &
-\ttindexboldpos{-->}{$HOL0imp} &
-\verb$~$\index{$HOL0not@\verb$~$|bold} &
-\verb$~=$\index{$HOL0noteq@\verb$~=$|bold} &
-\ttindexbold{ALL} &
-\texttt{!}\index{$HOL0All@\ttall|bold} &
-\ttindexbold{EX} &
-\texttt{?}\index{$HOL0Ex@\texttt{?}|bold} &
-\ttEXU\index{EXX@\ttEXU|bold} &
-\ttuniquex\index{$HOL0ExU@\ttuniquex|bold}\\
-\hline\hline
 \indexboldpos{\isasymlbrakk}{$Isabrl} &
+\texttt{[|}\index{$Isabrl@\ttlbr|bold} &
+\verb$\<lbrakk>$ \\
 \indexboldpos{\isasymrbrakk}{$Isabrr} &
+\texttt{|]}\index{$Isabrr@\ttrbr|bold} &
+\verb$\<rbrakk>$ \\
 \indexboldpos{\isasymImp}{$IsaImp} &
+\ttindexboldpos{==>}{$IsaImp} &
+\verb$\<Longrightarrow>$ \\
 \indexboldpos{\isasymAnd}{$IsaAnd} &
+\texttt{!!}\index{$IsaAnd@\ttAnd|bold} &
+\verb$\<And>$ \\
 \indexboldpos{\isasymequiv}{$IsaEq} &
+\ttindexboldpos{==}{$IsaEq} &
+\verb$\<equiv>$ \\
 \indexboldpos{\isasymlambda}{$Isalam} &
-\indexboldpos{\isasymFun}{$IsaFun}&
-&
-&
-&
-\\
-\texttt{[|}\index{$Isabrl@\ttlbr|bold} &
-\texttt{|]}\index{$Isabrr@\ttrbr|bold} &
-\ttindexboldpos{==>}{$IsaImp} &
-\texttt{!!}\index{$IsaAnd@\ttAnd|bold} &
-\ttindexboldpos{==}{$IsaEq} &
 \texttt{\%}\indexbold{$Isalam@\texttt{\%}} &
-\ttindexboldpos{=>}{$IsaFun}&
-&
-&
-&
- \\
-\hline\hline
+\verb$\<lambda>$ \\
+\indexboldpos{\isasymFun}{$IsaFun} &
+\ttindexboldpos{=>}{$IsaFun} &
+\verb$\<Rightarrow>$ \\
+\indexboldpos{\isasymand}{$HOL0and} &
+\texttt{\&}\indexbold{$HOL0and@{\texttt{\&}}} &
+\verb$\<and>$ \\
+\indexboldpos{\isasymor}{$HOL0or} &
+\texttt{|}\index{$HOL0or@\ttor|bold} &
+\verb$\<or>$ \\
+\indexboldpos{\isasymimp}{$HOL0imp} &
+\ttindexboldpos{-->}{$HOL0imp} &
+\verb$\<longrightarrow>$ \\
+\indexboldpos{\isasymnot}{$HOL0not} &
+\verb$~$\index{$HOL0not@\verb$~$|bold} &
+\verb$\<not>$ \\
+\indexboldpos{\isasymnoteq}{$HOL0noteq} &
+\verb$~=$\index{$HOL0noteq@\verb$~=$|bold} &
+\verb$\<noteq>$ \\
+\indexboldpos{\isasymforall}{$HOL0All} &
+\ttindexbold{ALL}, \texttt{!}\index{$HOL0All@\ttall|bold} &
+\verb$\<forall>$ \\
+\indexboldpos{\isasymexists}{$HOL0Ex} &
+\ttindexbold{EX}, \texttt{?}\index{$HOL0Ex@\texttt{?}|bold} &
+\verb$\<exists>$ \\
+\isasymuniqex\index{$HOL0ExU@\isasymuniqex|bold} &
+\ttEXU\index{EXX@\ttEXU|bold}, \ttuniquex\index{$HOL0ExU@\ttuniquex|bold} &
+\verb$\<exists>!$\\
+\indexboldpos{\isasymepsilon}{$HOL0ExSome} &
+\ttindexbold{SOME} &
+\verb$\<?>$\\
 \indexboldpos{\isasymcirc}{$HOL1} &
+\ttindexbold{o} &
+\verb$\<?>$\\
 \indexboldpos{\isasymle}{$HOL2arithrel}&
+\ttindexboldpos{<=}{$HOL2arithrel}&
+\verb$\<le>$\\
 \indexboldpos{\isasymtimes}{$IsaFun}&
-&
-&
-&
-&
-&
-&
-&
- \\
-\ttindexbold{o} &
-\ttindexboldpos{<=}{$HOL2arithrel}&
 \ttindexboldpos{*}{$HOL2arithfun} &
-&
-&
-&
-&
-&
-&
-&
-\\
+\verb$\<times>$\\
+\indexboldpos{\isasymin}{$HOL3Set}&
+\ttindexboldpos{:}{$HOL3Set} &
+\verb$\<in>$\\
+? & %\indexboldpos{\isasymnotin}{$HOL3Set} fails for some strange reason
+\verb$~:$\index{$HOL3Set@\verb$~:$|bold} &
+\verb$\<notin>$\\
+\indexboldpos{\isasymsubseteq}{$HOL3Set}&
+\verb$<=$ &
+\verb$\<subseteq>$\\
+\indexboldpos{\isasymunion}{$HOL3Set}&
+\ttindexbold{Un} &
+\verb$\<union>$\\
+\indexboldpos{\isasyminter}{$HOL3Set}&
+\ttindexbold{Int} &
+\verb$\<inter>$\\
+\indexboldpos{\isasymUnion}{$HOL3Set}&
+\ttindexbold{UN}, \ttindexbold{Union} &
+\verb$\<Union>$\\
+\indexboldpos{\isasymInter}{$HOL3Set}&
+\ttindexbold{INT}, \ttindexbold{Inter} &
+\verb$\<Inter>$\\
 \hline
 \end{tabular}
 \end{center}
-\caption{Mathematical symbols and their ASCII-equivalents}
+\caption{Mathematical symbols, their ASCII-equivalents and ProofGeneral codes}
 \label{fig:ascii}
 \end{figure}\indexbold{ASCII symbols}
 

--- a/doc-src/TutorialI/tutorial.tex	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/tutorial.tex	Mon Oct 09 10:18:21 2000 +0200
@@ -65,7 +65,7 @@
 
 \input{basics}
 \input{fp}
-%\input{CTL/ctl}
+\input{CTL/ctl}
 \input{Advanced/advanced}
 %\chapter{The Tricks of the Trade}
 \input{appendix}