apply. -> by

--- a/doc-src/TutorialI/CodeGen/CodeGen.thy	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/CodeGen/CodeGen.thy	Fri Jul 28 16:02:51 2000 +0200
@@ -105,7 +105,7 @@
 that contains two \isa{case}-expressions over instructions. Thus we add
 automatic case splitting as well, which finishes the proof:
 *}
-apply(induct_tac xs, simp, simp split: instr.split).;
+by(induct_tac xs, simp, simp split: instr.split);
 
 text{*\noindent
 Note that because \isaindex{auto} performs simplification, it can
@@ -116,7 +116,7 @@
 lemmas [simp del] = exec_app;
 lemma [simp]: "\\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"; 
 (*>*)
-apply(induct_tac xs, auto split: instr.split).;
+by(induct_tac xs, auto split: instr.split);
 
 text{*\noindent
 Although this is more compact, it is less clear for the reader of the proof.
@@ -128,6 +128,6 @@
 *}
 (*<*)
 theorem "\\<forall>vs. exec (comp e) s vs = (value e s) # vs";
-apply(induct_tac e, auto).;
+by(induct_tac e, auto);
 end
 (*>*)

--- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Fri Jul 28 16:02:51 2000 +0200
@@ -94,14 +94,14 @@
 that contains two \isa{case}-expressions over instructions. Thus we add
 automatic case splitting as well, which finishes the proof:%
 \end{isamarkuptxt}%
-\isacommand{apply}(induct\_tac~xs,~simp,~simp~split:~instr.split)\isacommand{.}%
+\isacommand{by}(induct\_tac~xs,~simp,~simp~split:~instr.split)%
 \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{apply}(induct\_tac~xs,~auto~split:~instr.split)\isacommand{.}%
+\isacommand{by}(induct\_tac~xs,~auto~split:~instr.split)%
 \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	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Datatype/ABexpr.thy	Fri Jul 28 16:02:51 2000 +0200
@@ -101,7 +101,7 @@
 The resulting 8 goals (one for each constructor) are proved in one fell swoop:
 *}
 
-apply auto.;
+by auto;
 
 text{*
 In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$,

--- a/doc-src/TutorialI/Datatype/Nested.thy	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Datatype/Nested.thy	Fri Jul 28 16:02:51 2000 +0200
@@ -60,7 +60,7 @@
 
 lemma "subst  Var t  = (t ::('a,'b)term)  \\<and>
         substs Var ts = (ts::('a,'b)term list)";
-apply(induct_tac t and ts, auto).;
+by(induct_tac t and ts, auto);
 
 text{*\noindent
 Note that \isa{Var} is the identity substitution because by definition it
@@ -88,7 +88,7 @@
 (*<*)
 
 lemma "subst s (App f ts) = App f (map (subst s) ts)";
-apply(induct_tac ts, auto).;
+by(induct_tac ts, auto);
 
 end
 (*>*)

--- a/doc-src/TutorialI/Datatype/document/ABexpr.tex	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex	Fri Jul 28 16:02:51 2000 +0200
@@ -91,7 +91,7 @@
 \noindent
 The resulting 8 goals (one for each constructor) are proved in one fell swoop:%
 \end{isamarkuptxt}%
-\isacommand{apply}~auto\isacommand{.}%
+\isacommand{by}~auto%
 \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/Nested.tex	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex	Fri Jul 28 16:02:51 2000 +0200
@@ -55,7 +55,7 @@
 \end{isamarkuptext}%
 \isacommand{lemma}~{"}subst~~Var~t~~=~(t~::('a,'b)term)~~{\isasymand}\isanewline
 ~~~~~~~~substs~Var~ts~=~(ts::('a,'b)term~list){"}\isanewline
-\isacommand{apply}(induct\_tac~t~\isakeyword{and}~ts,~auto)\isacommand{.}%
+\isacommand{by}(induct\_tac~t~\isakeyword{and}~ts,~auto)%
 \begin{isamarkuptext}%
 \noindent
 Note that \isa{Var} is the identity substitution because by definition it

--- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Fri Jul 28 16:02:51 2000 +0200
@@ -84,7 +84,7 @@
 *}
 
 apply(induct_tac b);
-apply(auto).;
+by(auto);
 
 text{*\noindent
 In fact, all proofs in this case study look exactly like this. Hence we do
@@ -127,11 +127,11 @@
   "\\<forall>t e. valif (normif b t e) env = valif (IF b t e) env";
 (*<*)
 apply(induct_tac b);
-apply(auto).;
+by(auto);
 
 theorem "valif (norm b) env = valif b env";
 apply(induct_tac b);
-apply(auto).;
+by(auto);
 (*>*)
 text{*\noindent
 Note that the lemma does not have a name, but is implicitly used in the proof
@@ -153,14 +153,14 @@
 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).;
+by(auto);
 
 theorem "normal(norm b)";
 apply(induct_tac b);
-apply(auto).;
+by(auto);
 
 end
 (*>*)

--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Fri Jul 28 16:02:51 2000 +0200
@@ -74,7 +74,7 @@
 The proof is canonical:%
 \end{isamarkuptxt}%
 \isacommand{apply}(induct\_tac~b)\isanewline
-\isacommand{apply}(auto)\isacommand{.}%
+\isacommand{by}(auto)%
 \begin{isamarkuptext}%
 \noindent
 In fact, all proofs in this case study look exactly like this. Hence we do
@@ -131,7 +131,7 @@
 and prove \isa{normal(norm b)}. Of course, this requires a lemma about
 normality of \isa{normif}:%
 \end{isamarkuptext}%
-\isacommand{lemma}~[simp]:~{"}{\isasymforall}t~e.~normal(normif~b~t~e)~=~(normal~t~{\isasymand}~normal~e){"}\end{isabelle}%
+\isacommand{lemma}[simp]:~{"}{\isasymforall}t~e.~normal(normif~b~t~e)~=~(normal~t~{\isasymand}~normal~e){"}\end{isabelle}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"

--- a/doc-src/TutorialI/Misc/Itrev.thy	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/Itrev.thy	Fri Jul 28 16:02:51 2000 +0200
@@ -5,7 +5,7 @@
 text{*
 We define a tail-recursive version of list-reversal,
 i.e.\ one that can be compiled into a loop:
-*}
+*};
 
 consts itrev :: "'a list \\<Rightarrow> 'a list \\<Rightarrow> 'a list";
 primrec
@@ -18,13 +18,13 @@
 argument when the first one becomes empty.
 We need to show that \isa{itrev} does indeed reverse its first argument
 provided the second one is empty:
-*}
+*};
 
 lemma "itrev xs [] = rev xs";
 
 txt{*\noindent
 There is no choice as to the induction variable, and we immediately simplify:
-*}
+*};
 
 apply(induct_tac xs, auto);
 
@@ -42,7 +42,7 @@
 
 Of course one cannot do this na\"{\i}vely: \isa{itrev xs ys = rev xs} is
 just not true---the correct generalization is
-*}
+*};
 (*<*)oops;(*>*)
 lemma "itrev xs ys = rev xs @ ys";
 
@@ -67,7 +67,7 @@
 the subgoal, but the induction hypothesis needs to be applied with
 \isa{a \# ys} instead of \isa{ys}. Hence we prove the theorem
 for all \isa{ys} instead of a fixed one:
-*}
+*};
 (*<*)oops;(*>*)
 lemma "\\<forall>ys. itrev xs ys = rev xs @ ys";
 
@@ -82,9 +82,9 @@
 provability of the goal. Because it is not always required, and may even
 complicate matters in some cases, this heuristic is often not
 applied blindly.
-*}
+*};
 
 (*<*)
-oops;
+by(induct_tac xs, simp, simp);
 end
 (*>*)

--- a/doc-src/TutorialI/Misc/Tree.thy	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/Tree.thy	Fri Jul 28 16:02:51 2000 +0200
@@ -21,7 +21,7 @@
 lemma mirror_mirror: "mirror(mirror t) = t";
 (*<*)
 apply(induct_tac t);
-apply(auto).;
+by(auto);
 
 end
 (*>*)

--- a/doc-src/TutorialI/Misc/arith1.thy	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/arith1.thy	Fri Jul 28 16:02:51 2000 +0200
@@ -3,6 +3,6 @@
 (*>*)
 lemma "\\<lbrakk> \\<not> m < n; m < n+1 \\<rbrakk> \\<Longrightarrow> m = n";
 (**)(*<*)
-apply(auto).;
+by(auto);
 end
 (*>*)

--- a/doc-src/TutorialI/Misc/arith2.thy	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/arith2.thy	Fri Jul 28 16:02:51 2000 +0200
@@ -2,7 +2,7 @@
 theory arith2 = Main:;
 (*>*)
 lemma "min i (max j (k*k)) = max (min (k*k) i) (min i (j::nat))";
-apply(arith).;
+by(arith);
 (**)(*<*)
 end
 (*>*)

--- a/doc-src/TutorialI/Misc/arith4.thy	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/arith4.thy	Fri Jul 28 16:02:51 2000 +0200
@@ -3,6 +3,6 @@
 (*>*)
 lemma "\\<not> m < n \\<and> m < n+1 \\<Longrightarrow> m = n";
 (**)(*<*)
-oops;
+by(arith);
 end
 (*>*)

--- a/doc-src/TutorialI/Misc/asm_simp.thy	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/asm_simp.thy	Fri Jul 28 16:02:51 2000 +0200
@@ -7,7 +7,7 @@
 *}
 
 lemma "\\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \\<rbrakk> \\<Longrightarrow> ys = zs";
-apply simp.;
+by simp;
 
 text{*\noindent
 The second assumption simplifies to \isa{xs = []}, which in turn
@@ -28,7 +28,7 @@
 explicitly telling the simplifier to ignore the assumptions:
 *}
 
-apply(simp (no_asm)).;
+by(simp (no_asm));
 
 text{*\noindent
 There are three options that influence the treatment of assumptions:

--- a/doc-src/TutorialI/Misc/case_splits.thy	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/case_splits.thy	Fri Jul 28 16:02:51 2000 +0200
@@ -53,7 +53,7 @@
 (*<*)
 lemma "(case xs of [] \\<Rightarrow> zs | y#ys \\<Rightarrow> y#(ys@zs)) = xs@zs";
 (*>*)
-apply(simp split: list.split).;
+by(simp split: list.split);
 
 text{*\noindent%
 which \isacommand{apply}\isa{(simp)} alone will not do.

--- a/doc-src/TutorialI/Misc/cases.thy	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/cases.thy	Fri Jul 28 16:02:51 2000 +0200
@@ -14,7 +14,7 @@
 which is solved automatically:
 *}
 
-apply(auto).;
+by(auto);
 (**)
 (*<*)
 end

--- a/doc-src/TutorialI/Misc/cond_rewr.thy	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/cond_rewr.thy	Fri Jul 28 16:02:51 2000 +0200
@@ -8,7 +8,7 @@
 *}
 
 lemma hd_Cons_tl[simp]: "xs \\<noteq> []  \\<Longrightarrow>  hd xs # tl xs = xs";
-apply(case_tac xs, simp, simp).;
+by(case_tac xs, simp, simp);
 
 text{*\noindent
 Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a
@@ -20,7 +20,7 @@
 
 lemma "xs \\<noteq> [] \\<Longrightarrow> hd(rev xs) # tl(rev xs) = rev xs";
 (*<*)
-apply(simp).
+by(simp);
 (*>*)
 text{*\noindent
 is proved by plain simplification:

--- a/doc-src/TutorialI/Misc/document/arith2.tex	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/arith2.tex	Fri Jul 28 16:02:51 2000 +0200
@@ -1,6 +1,6 @@
 \begin{isabelle}%
 \isacommand{lemma}~{"}min~i~(max~j~(k*k))~=~max~(min~(k*k)~i)~(min~i~(j::nat)){"}\isanewline
-\isacommand{apply}(arith)\isacommand{.}\isanewline
+\isacommand{by}(arith)\isanewline
 \end{isabelle}%
 %%% Local Variables:
 %%% mode: latex

--- a/doc-src/TutorialI/Misc/document/asm_simp.tex	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/asm_simp.tex	Fri Jul 28 16:02:51 2000 +0200
@@ -5,7 +5,7 @@
 as simplification rules and are simplified themselves. For example:%
 \end{isamarkuptext}%
 \isacommand{lemma}~{"}{\isasymlbrakk}~xs~@~zs~=~ys~@~xs;~[]~@~xs~=~[]~@~[]~{\isasymrbrakk}~{\isasymLongrightarrow}~ys~=~zs{"}\isanewline
-\isacommand{apply}~simp\isacommand{.}%
+\isacommand{by}~simp%
 \begin{isamarkuptext}%
 \noindent
 The second assumption simplifies to \isa{xs = []}, which in turn
@@ -24,7 +24,7 @@
 nontermination but not this one. The problem can be circumvented by
 explicitly telling the simplifier to ignore the assumptions:%
 \end{isamarkuptxt}%
-\isacommand{apply}(simp~(no\_asm))\isacommand{.}%
+\isacommand{by}(simp~(no\_asm))%
 \begin{isamarkuptext}%
 \noindent
 There are three options that influence the treatment of assumptions:

--- a/doc-src/TutorialI/Misc/document/case_splits.tex	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/case_splits.tex	Fri Jul 28 16:02:51 2000 +0200
@@ -43,7 +43,7 @@
 in case of recursive datatypes. Again, if the \isa{only:} modifier is
 dropped, the above goal is solved,%
 \end{isamarkuptext}%
-\isacommand{apply}(simp~split:~list.split)\isacommand{.}%
+\isacommand{by}(simp~split:~list.split)%
 \begin{isamarkuptext}%
 \noindent%
 which \isacommand{apply}\isa{(simp)} alone will not do.

--- a/doc-src/TutorialI/Misc/document/cases.tex	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/cases.tex	Fri Jul 28 16:02:51 2000 +0200
@@ -11,7 +11,7 @@
 \end{isabellepar}%
 which is solved automatically:%
 \end{isamarkuptxt}%
-\isacommand{apply}(auto)\isacommand{.}\isanewline
+\isacommand{by}(auto)\isanewline
 \end{isabelle}%
 %%% Local Variables:
 %%% mode: latex

--- a/doc-src/TutorialI/Misc/document/cond_rewr.tex	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/cond_rewr.tex	Fri Jul 28 16:02:51 2000 +0200
@@ -5,7 +5,7 @@
 accepts \emph{conditional} equations, for example%
 \end{isamarkuptext}%
 \isacommand{lemma}~hd\_Cons\_tl[simp]:~{"}xs~{\isasymnoteq}~[]~~{\isasymLongrightarrow}~~hd~xs~\#~tl~xs~=~xs{"}\isanewline
-\isacommand{apply}(case\_tac~xs,~simp,~simp)\isacommand{.}%
+\isacommand{by}(case\_tac~xs,~simp,~simp)%
 \begin{isamarkuptext}%
 \noindent
 Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a

--- a/doc-src/TutorialI/Misc/document/let_rewr.tex	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/let_rewr.tex	Fri Jul 28 16:02:51 2000 +0200
@@ -1,6 +1,6 @@
 \begin{isabelle}%
 \isacommand{lemma}~{"}(let~xs~=~[]~in~xs@ys@xs)~=~ys{"}\isanewline
-\isacommand{apply}(simp~add:~Let\_def)\isacommand{.}%
+\isacommand{by}(simp~add:~Let\_def)%
 \begin{isamarkuptext}%
 If, in a particular context, there is no danger of a combinatorial explosion
 of nested \isa{let}s one could even add \isa{Let_def} permanently:%

--- a/doc-src/TutorialI/Misc/document/natsum.tex	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex	Fri Jul 28 16:02:51 2000 +0200
@@ -18,7 +18,7 @@
 \end{isamarkuptext}%
 \isacommand{lemma}~{"}sum~n~+~sum~n~=~n*(Suc~n){"}\isanewline
 \isacommand{apply}(induct\_tac~n)\isanewline
-\isacommand{apply}(auto)\isacommand{.}\isanewline
+\isacommand{by}(auto)\isanewline
 \end{isabelle}%
 %%% Local Variables:
 %%% mode: latex

--- a/doc-src/TutorialI/Misc/document/prime_def.tex	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/prime_def.tex	Fri Jul 28 16:02:51 2000 +0200
@@ -1,14 +1,14 @@
 \begin{isabelle}%
 \isanewline
-~~~~{"}prime(p)~{\isasymequiv}~1~<~p~{\isasymand}~((m~dvd~p)~{\isasymlongrightarrow}~(m=1~{\isasymor}~m=p)){"}%
+~~~~{"}prime(p)~{\isasymequiv}~1~<~p~{\isasymand}~(m~dvd~p~{\isasymlongrightarrow}~(m=1~{\isasymor}~m=p)){"}%
 \begin{isamarkuptext}%
 \noindent\small
 where \isa{dvd} means ``divides''.
 Isabelle rejects this ``definition'' because of the extra \isa{m} on the
-right-hand side, which would introduce an inconsistency. (Why?) What you
+right-hand side, which would introduce an inconsistency (why?). What you
 should have written is%
 \end{isamarkuptext}%
-~{"}prime(p)~{\isasymequiv}~1~<~p~{\isasymand}~({\isasymforall}m.~(m~dvd~p)~{\isasymlongrightarrow}~(m=1~{\isasymor}~m=p)){"}\end{isabelle}%
+~{"}prime(p)~{\isasymequiv}~1~<~p~{\isasymand}~({\isasymforall}m.~m~dvd~p~{\isasymlongrightarrow}~(m=1~{\isasymor}~m=p)){"}\end{isabelle}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"

--- a/doc-src/TutorialI/Misc/let_rewr.thy	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/let_rewr.thy	Fri Jul 28 16:02:51 2000 +0200
@@ -2,7 +2,7 @@
 theory let_rewr = Main:;
 (*>*)
 lemma "(let xs = [] in xs@ys@xs) = ys";
-apply(simp add: Let_def).;
+by(simp add: Let_def);
 
 text{*
 If, in a particular context, there is no danger of a combinatorial explosion

--- a/doc-src/TutorialI/Misc/natsum.thy	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/natsum.thy	Fri Jul 28 16:02:51 2000 +0200
@@ -21,7 +21,7 @@
 
 lemma "sum n + sum n = n*(Suc n)";
 apply(induct_tac n);
-apply(auto).;
+by(auto);
 
 (*<*)
 end

--- a/doc-src/TutorialI/Misc/prime_def.thy	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/prime_def.thy	Fri Jul 28 16:02:51 2000 +0200
@@ -4,15 +4,15 @@
 (*>*)
 (*<*)term(*>*)
 
-    "prime(p) \\<equiv> 1 < p \\<and> ((m dvd p) \\<longrightarrow> (m=1 \\<or> m=p))";
+    "prime(p) \\<equiv> 1 < p \\<and> (m dvd p \\<longrightarrow> (m=1 \\<or> m=p))";
 text{*\noindent\small
 where \isa{dvd} means ``divides''.
 Isabelle rejects this ``definition'' because of the extra \isa{m} on the
-right-hand side, which would introduce an inconsistency. (Why?) What you
+right-hand side, which would introduce an inconsistency (why?). What you
 should have written is
 *}
 (*<*)term(*>*)
- "prime(p) \\<equiv> 1 < p \\<and> (\\<forall>m. (m dvd p) \\<longrightarrow> (m=1 \\<or> m=p))"
+ "prime(p) \\<equiv> 1 < p \\<and> (\\<forall>m. m dvd p \\<longrightarrow> (m=1 \\<or> m=p))"
 (*<*)
 end
 (*>*)

--- a/doc-src/TutorialI/Recdef/Induction.thy	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Induction.thy	Fri Jul 28 16:02:51 2000 +0200
@@ -41,7 +41,7 @@
 The rest is pure simplification:
 *}
 
-apply auto.;
+by auto;
 
 text{*
 Try proving the above lemma by structural induction, and you find that you

--- a/doc-src/TutorialI/Recdef/document/Induction.tex	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Induction.tex	Fri Jul 28 16:02:51 2000 +0200
@@ -36,7 +36,7 @@
 \end{isabellepar}%
 The rest is pure simplification:%
 \end{isamarkuptxt}%
-\isacommand{apply}~auto\isacommand{.}%
+\isacommand{by}~auto%
 \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/simplification.tex	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex	Fri Jul 28 16:02:51 2000 +0200
@@ -79,9 +79,9 @@
 derived conditional ones. For \isa{gcd} it means we have to prove%
 \end{isamarkuptext}%
 \isacommand{lemma}~[simp]:~{"}gcd~(m,~0)~=~m{"}\isanewline
-\isacommand{apply}(simp)\isacommand{.}\isanewline
+\isacommand{by}(simp)\isanewline
 \isacommand{lemma}~[simp]:~{"}n~{\isasymnoteq}~0~{\isasymLongrightarrow}~gcd(m,~n)~=~gcd(n,~m~mod~n){"}\isanewline
-\isacommand{apply}(simp)\isacommand{.}%
+\isacommand{by}(simp)%
 \begin{isamarkuptext}%
 \noindent
 after which we can disable the original simplification rule:%

--- a/doc-src/TutorialI/Recdef/document/termination.tex	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/termination.tex	Fri Jul 28 16:02:51 2000 +0200
@@ -31,7 +31,7 @@
 It was not proved automatically because of the special nature of \isa{-}
 on \isa{nat}. This requires more arithmetic than is tried by default:%
 \end{isamarkuptxt}%
-\isacommand{apply}(arith)\isacommand{.}%
+\isacommand{by}(arith)%
 \begin{isamarkuptext}%
 \noindent
 Because \isacommand{recdef}'s termination prover involves simplification,
@@ -48,7 +48,7 @@
 rules. Thus we can automatically prove%
 \end{isamarkuptext}%
 \isacommand{theorem}~wow:~{"}g(1,0)~=~g(1,1){"}\isanewline
-\isacommand{apply}(simp)\isacommand{.}%
+\isacommand{by}(simp)%
 \begin{isamarkuptext}%
 \noindent
 More exciting theorems require induction, which is discussed below.

--- a/doc-src/TutorialI/Recdef/simplification.thy	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Recdef/simplification.thy	Fri Jul 28 16:02:51 2000 +0200
@@ -90,9 +90,9 @@
 *}
 
 lemma [simp]: "gcd (m, 0) = m";
-apply(simp).;
+by(simp);
 lemma [simp]: "n \\<noteq> 0 \\<Longrightarrow> gcd(m, n) = gcd(n, m mod n)";
-apply(simp).;
+by(simp);
 
 text{*\noindent
 after which we can disable the original simplification rule:

--- a/doc-src/TutorialI/Recdef/termination.thy	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Recdef/termination.thy	Fri Jul 28 16:02:51 2000 +0200
@@ -36,7 +36,7 @@
 on \isa{nat}. This requires more arithmetic than is tried by default:
 *}
 
-apply(arith).;
+by(arith);
 
 text{*\noindent
 Because \isacommand{recdef}'s termination prover involves simplification,
@@ -55,7 +55,7 @@
 *}
 
 theorem wow: "g(1,0) = g(1,1)";
-apply(simp).;
+by(simp);
 
 text{*\noindent
 More exciting theorems require induction, which is discussed below.

--- a/doc-src/TutorialI/ToyList/ToyList.thy	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/ToyList/ToyList.thy	Fri Jul 28 16:02:51 2000 +0200
@@ -286,7 +286,9 @@
 just proved with its name. Notice that in the lemma \isa{app_Nil2} (as
 printed out after the final dot) the free variable \isa{xs} has been
 replaced by the unknown \isa{?xs}, just as explained in
-\S\ref{sec:variables}.
+\S\ref{sec:variables}. Note that instead of instead of \isacommand{apply}
+followed by a dot, you can simply write \isacommand{by}\indexbold{by},
+which we do most of the time.
 
 Going back to the proof of the first lemma
 *}
@@ -324,7 +326,7 @@
 
 lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)";
 apply(induct_tac xs);
-apply(auto).;
+by(auto);
 
 text{*
 \noindent
@@ -335,7 +337,7 @@
 
 lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
 apply(induct_tac xs);
-apply(auto).;
+by(auto);
 
 text{*\noindent
 and then solve our main theorem:
@@ -343,7 +345,7 @@
 
 theorem rev_rev [simp]: "rev(rev xs) = xs";
 apply(induct_tac xs);
-apply(auto).;
+by(auto);
 
 text{*\noindent
 The final \isa{end} tells Isabelle to close the current theory because

--- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Fri Jul 28 16:02:51 2000 +0200
@@ -265,7 +265,9 @@
 just proved with its name. Notice that in the lemma \isa{app_Nil2} (as
 printed out after the final dot) the free variable \isa{xs} has been
 replaced by the unknown \isa{?xs}, just as explained in
-\S\ref{sec:variables}.
+\S\ref{sec:variables}. Note that instead of instead of \isacommand{apply}
+followed by a dot, you can simply write \isacommand{by}\indexbold{by},
+which we do most of the time.
 
 Going back to the proof of the first lemma%
 \end{isamarkuptext}%
@@ -299,7 +301,7 @@
 \end{comment}
 \isacommand{lemma}~app\_assoc~[simp]:~{"}(xs~@~ys)~@~zs~=~xs~@~(ys~@~zs){"}\isanewline
 \isacommand{apply}(induct\_tac~xs)\isanewline
-\isacommand{apply}(auto)\isacommand{.}%
+\isacommand{by}(auto)%
 \begin{isamarkuptext}%
 \noindent
 succeeds without further ado.
@@ -308,14 +310,14 @@
 \end{isamarkuptext}%
 \isacommand{lemma}~rev\_app~[simp]:~{"}rev(xs~@~ys)~=~(rev~ys)~@~(rev~xs){"}\isanewline
 \isacommand{apply}(induct\_tac~xs)\isanewline
-\isacommand{apply}(auto)\isacommand{.}%
+\isacommand{by}(auto)%
 \begin{isamarkuptext}%
 \noindent
 and then solve our main theorem:%
 \end{isamarkuptext}%
 \isacommand{theorem}~rev\_rev~[simp]:~{"}rev(rev~xs)~=~xs{"}\isanewline
 \isacommand{apply}(induct\_tac~xs)\isanewline
-\isacommand{apply}(auto)\isacommand{.}%
+\isacommand{by}(auto)%
 \begin{isamarkuptext}%
 \noindent
 The final \isa{end} tells Isabelle to close the current theory because

--- a/doc-src/TutorialI/ToyList2/ToyList2	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/ToyList2/ToyList2	Fri Jul 28 16:02:51 2000 +0200
@@ -1,17 +1,18 @@
 lemma app_Nil2 [simp]: "xs @ [] = xs";
 apply(induct_tac xs);
-apply(auto);.;
+apply(auto);
+.;
 
 lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)";
 apply(induct_tac xs);
-apply(auto);.;
+by(auto);
 
 lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
 apply(induct_tac xs);
-apply(auto);.;
+by(auto);
 
 theorem rev_rev [simp]: "rev(rev xs) = xs";
 apply(induct_tac xs);
-apply(auto);.;
+by(auto);
 
 end;

--- a/doc-src/TutorialI/Trie/Trie.thy	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Trie/Trie.thy	Fri Jul 28 16:02:51 2000 +0200
@@ -7,7 +7,7 @@
 representation where the subtries are held in an association list, i.e.\ a
 list of (letter,trie) pairs.  Abstracting over the alphabet \isa{'a} and the
 values \isa{'v} we define a trie as follows:
-*}
+*};
 
 datatype ('a,'v)trie = Trie  "'v option"  "('a * ('a,'v)trie)list";
 
@@ -16,7 +16,7 @@
 association list of subtries.  This is an example of nested recursion involving products,
 which is fine because products are datatypes as well.
 We define two selector functions:
-*}
+*};
 
 consts value :: "('a,'v)trie \\<Rightarrow> 'v option"
        alist :: "('a,'v)trie \\<Rightarrow> ('a * ('a,'v)trie)list";
@@ -25,7 +25,7 @@
 
 text{*\noindent
 Association lists come with a generic lookup function:
-*}
+*};
 
 consts   assoc :: "('key * 'val)list \\<Rightarrow> 'key \\<Rightarrow> 'val option";
 primrec "assoc [] x = None"
@@ -37,7 +37,7 @@
 examining the letters of the search string one by one. As
 recursion on lists is simpler than on tries, let us express this as primitive
 recursion on the search string argument:
-*}
+*};
 
 consts   lookup :: "('a,'v)trie \\<Rightarrow> 'a list \\<Rightarrow> 'v option";
 primrec "lookup t [] = value t"
@@ -49,16 +49,16 @@
 As a first simple property we prove that looking up a string in the empty
 trie \isa{Trie~None~[]} always returns \isa{None}. The proof merely
 distinguishes the two cases whether the search string is empty or not:
-*}
+*};
 
 lemma [simp]: "lookup (Trie None []) as = None";
-apply(case_tac as, auto).;
+by(case_tac as, auto);
 
 text{*
 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
 associated with that string:
-*}
+*};
 
 consts update :: "('a,'v)trie \\<Rightarrow> 'a list \\<Rightarrow> 'v \\<Rightarrow> ('a,'v)trie";
 primrec
@@ -79,7 +79,7 @@
 Before we start on any proofs about \isa{update} we tell the simplifier to
 expand all \isa{let}s and to split all \isa{case}-constructs over
 options:
-*}
+*};
 
 theorems [simp] = Let_def;
 theorems [split] = option.split;
@@ -91,7 +91,7 @@
 
 Our main goal is to prove the correct interaction of \isa{update} and
 \isa{lookup}:
-*}
+*};
 
 theorem "\\<forall>t v bs. lookup (update t as v) bs =
                     (if as=bs then Some v else lookup t bs)";
@@ -104,7 +104,7 @@
 if \isa{update} has already been simplified, which can only happen if
 \isa{as} is instantiated.
 The start of the proof is completely conventional:
-*}
+*};
 
 apply(induct_tac as, auto);
 
@@ -118,10 +118,10 @@
 Clearly, if we want to make headway we have to instantiate \isa{bs} as
 well now. It turns out that instead of induction, case distinction
 suffices:
-*}
+*};
 
 apply(case_tac[!] bs);
-apply(auto).;
+by(auto);
 
 text{*\noindent
 Both \isaindex{case_tac} and \isaindex{induct_tac}
@@ -136,8 +136,8 @@
 goals up in such a way that case distinction on \isa{bs} makes sense and
 solves the proof. Part~\ref{Isar} shows you how to write readable and stable
 proofs.
-*}
+*};
 
 (*<*)
-end
+end;
 (*>*)

--- a/doc-src/TutorialI/Trie/document/Trie.tex	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Trie/document/Trie.tex	Fri Jul 28 16:02:51 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}(case\_tac~as,~auto)\isacommand{.}%
+\isacommand{by}(case\_tac~as,~auto)%
 \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 +107,7 @@
 suffices:%
 \end{isamarkuptxt}%
 \isacommand{apply}(case\_tac[!]~bs)\isanewline
-\isacommand{apply}(auto)\isacommand{.}%
+\isacommand{by}(auto)%
 \begin{isamarkuptext}%
 \noindent
 Both \isaindex{case_tac} and \isaindex{induct_tac}

--- a/doc-src/TutorialI/fp.tex	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/fp.tex	Fri Jul 28 16:02:51 2000 +0200
@@ -472,6 +472,8 @@
 \subsection{Using the simplifier}
 \label{sec:SimpFeatures}
 
+\subsubsection{What is simplification}
+
 In its most basic form, simplification means repeated application of
 equations from left to right. For example, taking the rules for \isa{\at}
 and applying them to the term \isa{[0,1] \at\ []} results in a sequence of