tuned;

--- a/doc-src/TutorialI/Advanced/Partial.thy	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Advanced/Partial.thy	Fri Jan 18 18:30:19 2002 +0100
@@ -138,7 +138,7 @@
 *}
 
 lemma "wf(step1 f) \<longrightarrow> f(find(f,x)) = find(f,x)"
-apply(induct_tac f x rule:find.induct);
+apply(induct_tac f x rule: find.induct);
 apply simp
 done
 
@@ -193,7 +193,7 @@
 apply(rule_tac P = "\<lambda>(x,x'). x' = f x" and
                r = "inv_image (step1 f) fst" in while_rule);
 apply auto
-apply(simp add:inv_image_def step1_def)
+apply(simp add: inv_image_def step1_def)
 done
 
 text{*
@@ -202,7 +202,7 @@
 
 theorem "wf(step1 f) \<Longrightarrow> f(find2 f x) = find2 f x"
 apply(drule_tac x = x in lem)
-apply(auto simp add:find2_def)
+apply(auto simp add: find2_def)
 done
 
 text{* Let us conclude this section on partial functions by a

--- a/doc-src/TutorialI/Advanced/document/Partial.tex	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Advanced/document/Partial.tex	Fri Jan 18 18:30:19 2002 +0100
@@ -165,7 +165,7 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymlongrightarrow}\ f{\isacharparenleft}find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f\ x\ rule{\isacharcolon}find{\isachardot}induct{\isacharparenright}\isanewline
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f\ x\ rule{\isacharcolon}\ find{\isachardot}induct{\isacharparenright}\isanewline
 \isamarkupfalse%
 \isacommand{apply}\ simp\isanewline
 \isamarkupfalse%
@@ -236,7 +236,7 @@
 \isamarkupfalse%
 \isacommand{apply}\ auto\isanewline
 \isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}inv{\isacharunderscore}image{\isacharunderscore}def\ step{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}\isanewline
+\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ inv{\isacharunderscore}image{\isacharunderscore}def\ step{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}\isanewline
 \isamarkupfalse%
 \isacommand{done}\isamarkupfalse%
 %
@@ -248,7 +248,7 @@
 \isamarkupfalse%
 \isacommand{apply}{\isacharparenleft}drule{\isacharunderscore}tac\ x\ {\isacharequal}\ x\ \isakeyword{in}\ lem{\isacharparenright}\isanewline
 \isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}find{\isadigit{2}}{\isacharunderscore}def{\isacharparenright}\isanewline
+\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ find{\isadigit{2}}{\isacharunderscore}def{\isacharparenright}\isanewline
 \isamarkupfalse%
 \isacommand{done}\isamarkupfalse%
 %

--- a/doc-src/TutorialI/CTL/CTL.thy	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/CTL/CTL.thy	Fri Jan 18 18:30:19 2002 +0100
@@ -31,7 +31,8 @@
 This definition allows a succinct statement of the semantics of @{term AF}:
 \footnote{Do not be misled: neither datatypes nor recursive functions can be
 extended by new constructors or equations. This is just a trick of the
-presentation. In reality one has to define a new datatype and a new function.}
+presentation (see \S\ref{sec:doc-prep-suppress}). In reality one has to define
+a new datatype and a new function.}
 *};
 (*<*)
 consts valid :: "state \<Rightarrow> formula \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80);
@@ -165,7 +166,7 @@
  "s \<notin> lfp(af A) \<Longrightarrow> s \<notin> A \<and> (\<exists> t. (s,t) \<in> M \<and> t \<notin> lfp(af A))";
 apply(erule contrapos_np);
 apply(subst lfp_unfold[OF mono_af]);
-apply(simp add:af_def);
+apply(simp add: af_def);
 done;
 
 text{*\noindent
@@ -210,7 +211,7 @@
 From this proposition the original goal follows easily:
 *};
 
- apply(simp add:Paths_def, blast);
+ apply(simp add: Paths_def, blast);
 
 txt{*\noindent
 The new subgoal is proved by providing the witness @{term "path s Q"} for @{term p}:
@@ -242,7 +243,7 @@
 @{text fast} can prove the base case quickly:
 *};
 
- apply(fast intro:someI2_ex);
+ apply(fast intro: someI2_ex);
 
 txt{*\noindent
 What is worth noting here is that we have used \methdx{fast} rather than
@@ -285,14 +286,14 @@
  \<exists> p\<in>Paths s. \<forall> i. Q(p i)";
 apply(subgoal_tac
  "\<exists> p. s = p 0 \<and> (\<forall> i. (p i,p(Suc i))\<in>M \<and> Q(p i))");
- apply(simp add:Paths_def);
+ apply(simp add: Paths_def);
  apply(blast);
 apply(rule_tac x = "nat_rec s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)" in exI);
 apply(simp);
 apply(intro strip);
 apply(induct_tac i);
  apply(simp);
- apply(fast intro:someI2_ex);
+ apply(fast intro: someI2_ex);
 apply(simp);
 apply(rule someI2_ex);
  apply(blast);
@@ -328,7 +329,7 @@
 Both are solved automatically:
 *};
 
- apply(auto dest:not_in_lfp_afD);
+ apply(auto dest: not_in_lfp_afD);
 done;
 
 text{*
@@ -388,7 +389,7 @@
 
 lemma "lfp(eufix A B) \<subseteq> eusem A B"
 apply(rule lfp_lowerbound)
-apply(clarsimp simp add:eusem_def eufix_def);
+apply(clarsimp simp add: eusem_def eufix_def);
 apply(erule disjE);
  apply(rule_tac x = "[]" in exI);
  apply simp
@@ -403,15 +404,15 @@
 done
 
 lemma "eusem A B \<subseteq> lfp(eufix A B)";
-apply(clarsimp simp add:eusem_def);
+apply(clarsimp simp add: eusem_def);
 apply(erule rev_mp);
 apply(rule_tac x = x in spec);
 apply(induct_tac p);
  apply(subst lfp_unfold[OF mono_eufix])
- apply(simp add:eufix_def);
+ apply(simp add: eufix_def);
 apply(clarsimp);
 apply(subst lfp_unfold[OF mono_eufix])
-apply(simp add:eufix_def);
+apply(simp add: eufix_def);
 apply blast;
 done
 
@@ -429,7 +430,7 @@
 "apath s (Suc i) = (SOME t. (apath s i,t) \<in> M)"
 
 lemma [iff]: "apath s \<in> Paths s";
-apply(simp add:Paths_def);
+apply(simp add: Paths_def);
 apply(blast intro: M_total[THEN someI_ex])
 done
 
@@ -438,11 +439,11 @@
 "pcons s p == \<lambda>i. case i of 0 \<Rightarrow> s | Suc j \<Rightarrow> p j"
 
 lemma pcons_PathI: "[| (s,t) : M; p \<in> Paths t |] ==> pcons s p \<in> Paths s";
-by(simp add:Paths_def pcons_def split:nat.split);
+by(simp add: Paths_def pcons_def split: nat.split);
 
 lemma "lfp(eufix A B) \<subseteq> eusem A B"
 apply(rule lfp_lowerbound)
-apply(clarsimp simp add:eusem_def eufix_def);
+apply(clarsimp simp add: eusem_def eufix_def);
 apply(erule disjE);
  apply(rule_tac x = "apath x" in bexI);
   apply(rule_tac x = 0 in exI);
@@ -451,8 +452,8 @@
 apply(clarify);
 apply(rule_tac x = "pcons xb p" in bexI);
  apply(rule_tac x = "j+1" in exI);
- apply (simp add:pcons_def split:nat.split);
-apply (simp add:pcons_PathI)
+ apply (simp add: pcons_def split: nat.split);
+apply (simp add: pcons_PathI)
 done
 *)
 (*>*)

--- a/doc-src/TutorialI/CTL/CTLind.thy	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/CTL/CTLind.thy	Fri Jan 18 18:30:19 2002 +0100
@@ -47,7 +47,7 @@
  apply(blast);
 apply(clarify);
 apply(drule_tac x = "\<lambda>i. case i of 0 \<Rightarrow> t | Suc i \<Rightarrow> f i" in bspec);
-apply(simp_all add:Paths_def split:nat.split);
+apply(simp_all add: Paths_def split: nat.split);
 done
 
 text{*\noindent
@@ -106,7 +106,7 @@
 
  apply(subst lfp_unfold[OF mono_af]);
  apply(simp (no_asm) add: af_def);
- apply(blast intro:Avoid.intros);
+ apply(blast intro: Avoid.intros);
 
 txt{*
 Having proved the main goal, we return to the proof obligation that the 
@@ -120,10 +120,10 @@
 *}
 
 apply(erule contrapos_pp);
-apply(simp add:wf_iff_no_infinite_down_chain);
+apply(simp add: wf_iff_no_infinite_down_chain);
 apply(erule exE);
 apply(rule ex_infinite_path);
-apply(auto simp add:Paths_def);
+apply(auto simp add: Paths_def);
 done
 
 text{*
@@ -140,7 +140,7 @@
 \index{CTL|)}*}
 
 theorem AF_lemma2:  "{s. \<forall>p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)";
-by(auto elim:Avoid_in_lfp intro:Avoid.intros);
+by(auto elim: Avoid_in_lfp intro: Avoid.intros);
 
 
 (*<*)end(*>*)

--- a/doc-src/TutorialI/CTL/PDL.thy	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/CTL/PDL.thy	Fri Jan 18 18:30:19 2002 +0100
@@ -174,7 +174,7 @@
 
 theorem "mc f = {s. s \<Turnstile> f}"
 apply(induct_tac f)
-apply(auto simp add:EF_lemma)
+apply(auto simp add: EF_lemma)
 done
 
 text{*

--- a/doc-src/TutorialI/CTL/document/CTL.tex	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/CTL/document/CTL.tex	Fri Jan 18 18:30:19 2002 +0100
@@ -34,7 +34,8 @@
 This definition allows a succinct statement of the semantics of \isa{AF}:
 \footnote{Do not be misled: neither datatypes nor recursive functions can be
 extended by new constructors or equations. This is just a trick of the
-presentation. In reality one has to define a new datatype and a new function.}%
+presentation (see \S\ref{sec:doc-prep-suppress}). In reality one has to define
+a new datatype and a new function.}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isamarkupfalse%
@@ -178,7 +179,7 @@
 \isamarkupfalse%
 \isacommand{apply}{\isacharparenleft}subst\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharparenright}\isanewline
 \isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}af{\isacharunderscore}def{\isacharparenright}\isanewline
+\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ af{\isacharunderscore}def{\isacharparenright}\isanewline
 \isamarkupfalse%
 \isacommand{done}\isamarkupfalse%
 %
@@ -229,7 +230,7 @@
 From this proposition the original goal follows easily:%
 \end{isamarkuptxt}%
 \ \isamarkuptrue%
-\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharcomma}\ blast{\isacharparenright}\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ Paths{\isacharunderscore}def{\isacharcomma}\ blast{\isacharparenright}\isamarkupfalse%
 %
 \begin{isamarkuptxt}%
 \noindent
@@ -275,7 +276,7 @@
 \isa{fast} can prove the base case quickly:%
 \end{isamarkuptxt}%
 \ \isamarkuptrue%
-\isacommand{apply}{\isacharparenleft}fast\ intro{\isacharcolon}someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}fast\ intro{\isacharcolon}\ someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}\isamarkupfalse%
 %
 \begin{isamarkuptxt}%
 \noindent
@@ -375,7 +376,7 @@
 Both are solved automatically:%
 \end{isamarkuptxt}%
 \ \isamarkuptrue%
-\isacommand{apply}{\isacharparenleft}auto\ dest{\isacharcolon}not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharparenright}\isanewline
+\isacommand{apply}{\isacharparenleft}auto\ dest{\isacharcolon}\ not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharparenright}\isanewline
 \isamarkupfalse%
 \isacommand{done}\isamarkupfalse%
 %

--- a/doc-src/TutorialI/CTL/document/CTLind.tex	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/CTL/document/CTLind.tex	Fri Jan 18 18:30:19 2002 +0100
@@ -58,7 +58,7 @@
 \isamarkupfalse%
 \isacommand{apply}{\isacharparenleft}drule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}{\isasymlambda}i{\isachardot}\ case\ i\ of\ {\isadigit{0}}\ {\isasymRightarrow}\ t\ {\isacharbar}\ Suc\ i\ {\isasymRightarrow}\ f\ i{\isachardoublequote}\ \isakeyword{in}\ bspec{\isacharparenright}\isanewline
 \isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}Paths{\isacharunderscore}def\ split{\isacharcolon}nat{\isachardot}split{\isacharparenright}\isanewline
+\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ Paths{\isacharunderscore}def\ split{\isacharcolon}\ nat{\isachardot}split{\isacharparenright}\isanewline
 \isamarkupfalse%
 \isacommand{done}\isamarkupfalse%
 %
@@ -133,7 +133,7 @@
 \ \isamarkupfalse%
 \isacommand{apply}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}\ add{\isacharcolon}\ af{\isacharunderscore}def{\isacharparenright}\isanewline
 \ \isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}Avoid{\isachardot}intros{\isacharparenright}\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ Avoid{\isachardot}intros{\isacharparenright}\isamarkupfalse%
 %
 \begin{isamarkuptxt}%
 Having proved the main goal, we return to the proof obligation that the 
@@ -149,13 +149,13 @@
 \isamarkuptrue%
 \isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}pp{\isacharparenright}\isanewline
 \isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain{\isacharparenright}\isanewline
+\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain{\isacharparenright}\isanewline
 \isamarkupfalse%
 \isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline
 \isamarkupfalse%
 \isacommand{apply}{\isacharparenleft}rule\ ex{\isacharunderscore}infinite{\isacharunderscore}path{\isacharparenright}\isanewline
 \isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharparenright}\isanewline
+\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ Paths{\isacharunderscore}def{\isacharparenright}\isanewline
 \isamarkupfalse%
 \isacommand{done}\isamarkupfalse%
 %
@@ -177,7 +177,7 @@
 \isamarkuptrue%
 \isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharcolon}\ \ {\isachardoublequote}{\isacharbraceleft}s{\isachardot}\ {\isasymforall}p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}\ {\isasymsubseteq}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{by}{\isacharparenleft}auto\ elim{\isacharcolon}Avoid{\isacharunderscore}in{\isacharunderscore}lfp\ intro{\isacharcolon}Avoid{\isachardot}intros{\isacharparenright}\isanewline
+\isacommand{by}{\isacharparenleft}auto\ elim{\isacharcolon}\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp\ intro{\isacharcolon}\ Avoid{\isachardot}intros{\isacharparenright}\isanewline
 \isanewline
 \isamarkupfalse%
 \isamarkupfalse%

--- a/doc-src/TutorialI/CTL/document/PDL.tex	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/CTL/document/PDL.tex	Fri Jan 18 18:30:19 2002 +0100
@@ -217,7 +217,7 @@
 \isamarkupfalse%
 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline
 \isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}EF{\isacharunderscore}lemma{\isacharparenright}\isanewline
+\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ EF{\isacharunderscore}lemma{\isacharparenright}\isanewline
 \isamarkupfalse%
 \isacommand{done}\isamarkupfalse%
 %

--- a/doc-src/TutorialI/Inductive/AB.thy	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Inductive/AB.thy	Fri Jan 18 18:30:19 2002 +0100
@@ -165,7 +165,7 @@
     size[x\<in>take i w @ drop i w. \<not>P x]+2;
     size[x\<in>take i w. P x] = size[x\<in>take i w. \<not>P x]+1\<rbrakk>
    \<Longrightarrow> size[x\<in>drop i w. P x] = size[x\<in>drop i w. \<not>P x]+1"
-by(simp del:append_take_drop_id)
+by(simp del: append_take_drop_id)
 
 text{*\noindent
 In the proof we have disabled the normally useful lemma
@@ -280,8 +280,8 @@
  apply(assumption)
 apply(rule_tac n1=i and t=v in subst[OF append_take_drop_id])
 apply(rule S_A_B.intros)
- apply(force simp add:min_less_iff_disj)
-by(force simp add:min_less_iff_disj split add: nat_diff_split)
+ apply(force simp add: min_less_iff_disj)
+by(force simp add: min_less_iff_disj split add: nat_diff_split)
 
 text{*
 We conclude this section with a comparison of our proof with 

--- a/doc-src/TutorialI/Inductive/Mutual.thy	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Inductive/Mutual.thy	Fri Jan 18 18:30:19 2002 +0100
@@ -49,7 +49,7 @@
 (*<*)
   apply simp
  apply simp
-apply(simp add:dvd_def)
+apply(simp add: dvd_def)
 apply(clarify)
 apply(rule_tac x = "Suc k" in exI)
 apply simp

--- a/doc-src/TutorialI/Inductive/Star.thy	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Inductive/Star.thy	Fri Jan 18 18:30:19 2002 +0100
@@ -167,7 +167,7 @@
 lemma rtc_step2[rule_format]: "(x,y) : r* \<Longrightarrow> (y,z) : r --> (x,z) : r*"
 apply(erule rtc.induct);
  apply blast;
-apply(blast intro:rtc_step)
+apply(blast intro: rtc_step)
 done
 
 end

--- a/doc-src/TutorialI/Inductive/document/AB.tex	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Inductive/document/AB.tex	Fri Jan 18 18:30:19 2002 +0100
@@ -182,7 +182,7 @@
 \ \ \ \ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isasymrbrakk}\isanewline
 \ \ \ {\isasymLongrightarrow}\ size{\isacharbrackleft}x{\isasymin}drop\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}drop\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharparenright}\isamarkupfalse%
+\isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharparenright}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent
@@ -325,9 +325,9 @@
 \isamarkupfalse%
 \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}\isanewline
 \ \isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline
+\isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}\ min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline
 \isamarkupfalse%
-\isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isamarkupfalse%
+\isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}\ min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 We conclude this section with a comparison of our proof with 

--- a/doc-src/TutorialI/Misc/AdvancedInd.thy	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Misc/AdvancedInd.thy	Fri Jan 18 18:30:19 2002 +0100
@@ -80,8 +80,7 @@
 \forall y@1 \dots y@n.~ x = t \longrightarrow C.
 \end{equation}
 where $y@1 \dots y@n$ are the free variables in $t$ and $x$ is a new variable.
-Now you can perform
-perform induction on~$x$. An example appears in
+Now you can perform induction on~$x$. An example appears in
 \S\ref{sec:complete-ind} below.
 
 The very same problem may occur in connection with rule induction. Remember
@@ -264,7 +263,7 @@
 the induction hypothesis:
 *};
  apply(blast);
-by(blast elim:less_SucE)
+by(blast elim: less_SucE)
 
 text{*\noindent
 The elimination rule @{thm[source]less_SucE} expresses the case distinction:

--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Fri Jan 18 18:30:19 2002 +0100
@@ -92,8 +92,7 @@
 \forall y@1 \dots y@n.~ x = t \longrightarrow C.
 \end{equation}
 where $y@1 \dots y@n$ are the free variables in $t$ and $x$ is a new variable.
-Now you can perform
-perform induction on~$x$. An example appears in
+Now you can perform induction on~$x$. An example appears in
 \S\ref{sec:complete-ind} below.
 
 The very same problem may occur in connection with rule induction. Remember
@@ -309,7 +308,7 @@
 \ \isamarkuptrue%
 \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
 \isamarkupfalse%
-\isacommand{by}{\isacharparenleft}blast\ elim{\isacharcolon}less{\isacharunderscore}SucE{\isacharparenright}\isamarkupfalse%
+\isacommand{by}{\isacharparenleft}blast\ elim{\isacharcolon}\ less{\isacharunderscore}SucE{\isacharparenright}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent

--- a/doc-src/TutorialI/Overview/Ind.thy	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Overview/Ind.thy	Fri Jan 18 18:30:19 2002 +0100
@@ -93,7 +93,7 @@
 lemma "wf{(x,y). (x,y) \<in> r \<and> y \<in> acc r}"
 thm wfI
 apply(rule_tac A = "acc r" in wfI)
- apply (blast elim:acc.elims)
+ apply (blast elim: acc.elims)
 apply(simp(no_asm_use))
 thm acc.induct
 apply(erule acc.induct)

--- a/doc-src/TutorialI/Overview/Isar.thy	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Overview/Isar.thy	Fri Jan 18 18:30:19 2002 +0100
@@ -9,7 +9,7 @@
       (is "lfp ?F = ?toA")
 proof
   show "lfp ?F \<subseteq> ?toA"
-  by (blast intro!: lfp_lowerbound intro:rtrancl_trans)
+  by (blast intro!: lfp_lowerbound intro: rtrancl_trans)
 
   show "?toA \<subseteq> lfp ?F"
   proof

--- a/doc-src/TutorialI/Overview/RECDEF.thy	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Overview/RECDEF.thy	Fri Jan 18 18:30:19 2002 +0100
@@ -73,7 +73,7 @@
 
 lemma "mirror(mirror t) = t"
 apply(induct_tac t rule: mirror.induct)
-apply(simp add:rev_map sym[OF map_compose] cong:map_cong)
+apply(simp add: rev_map sym[OF map_compose] cong: map_cong)
 done
 
 text{*

--- a/doc-src/TutorialI/Overview/Sets.thy	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Overview/Sets.thy	Fri Jan 18 18:30:19 2002 +0100
@@ -102,7 +102,7 @@
 
 theorem "mc f = {s. s \<Turnstile> f}";
 apply(induct_tac f);
-apply(auto simp add:EF_lemma);
+apply(auto simp add: EF_lemma);
 done;
 
 text{*

--- a/doc-src/TutorialI/Protocol/protocol.tex	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Protocol/protocol.tex	Fri Jan 18 18:30:19 2002 +0100
@@ -324,6 +324,7 @@
 \isa{priK} maps agents to their private keys.  It is defined in terms of
 \isa{invKey} and \isa{pubK} by a translation; therefore \isa{priK} is
 not a proper constant, so we declare it using \isacommand{syntax}
+(cf.\ \S\ref{sec:syntax-translations}).
 \begin{isabelle}
 \isacommand{consts}\ \,pubK\ \ \ \ ::\ "agent\ =>\ key"\isanewline
 \isacommand{syntax}\ priK\ \ \ \ ::\ "agent\ =>\ key"\isanewline

--- a/doc-src/TutorialI/Recdef/Nested2.thy	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Recdef/Nested2.thy	Fri Jan 18 18:30:19 2002 +0100
@@ -19,13 +19,13 @@
 *}
 
 lemma "trev(trev t) = t"
-apply(induct_tac t rule:trev.induct)
+apply(induct_tac t rule: trev.induct)
 txt{*
 @{subgoals[display,indent=0]}
 Both the base case and the induction step fall to simplification:
 *}
 
-by(simp_all add:rev_map sym[OF map_compose] cong:map_cong)
+by(simp_all add: rev_map sym[OF map_compose] cong: map_cong)
 
 text{*\noindent
 If the proof of the induction step mystifies you, we recommend that you go through

--- a/doc-src/TutorialI/Recdef/document/Nested2.tex	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Recdef/document/Nested2.tex	Fri Jan 18 18:30:19 2002 +0100
@@ -20,7 +20,7 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}trev{\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ rule{\isacharcolon}trev{\isachardot}induct{\isacharparenright}\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ rule{\isacharcolon}\ trev{\isachardot}induct{\isacharparenright}\isamarkupfalse%
 %
 \begin{isamarkuptxt}%
 \begin{isabelle}%
@@ -32,7 +32,7 @@
 Both the base case and the induction step fall to simplification:%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}rev{\isacharunderscore}map\ sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}\ cong{\isacharcolon}map{\isacharunderscore}cong{\isacharparenright}\isamarkupfalse%
+\isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ rev{\isacharunderscore}map\ sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}\ cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent

--- a/doc-src/TutorialI/Rules/rules.tex	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex	Fri Jan 18 18:30:19 2002 +0100
@@ -1245,7 +1245,7 @@
 ``the greatest divisior of~$n$.''
 It returns an arbitrary value unless the formula has a unique solution.
 An \textbf{indefinite description} formalizes the word ``some,'' as in
-``some member of~$S$.''  It differs from a definition description in not
+``some member of~$S$.''  It differs from a definite description in not
 requiring the solution to be unique: it uses the axiom of choice to pick any
 solution. 
 

--- a/doc-src/TutorialI/Sets/Examples.thy	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Sets/Examples.thy	Fri Jan 18 18:30:19 2002 +0100
@@ -90,7 +90,7 @@
 text{*A type constraint lets it work*}
 
 text{*An issue here: how do we discuss the distinction between ASCII and
-X-symbol notation?  Here the latter disambiguates.*}
+symbol notation?  Here the latter disambiguates.*}
 
 
 text{*

--- a/doc-src/TutorialI/Sets/sets.tex	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex	Fri Jan 18 18:30:19 2002 +0100
@@ -51,7 +51,7 @@
 \end{isabelle}
 
 Here are two of the many installed theorems concerning set
-complement.\index{complement!of a set}%
+complement.\index{complement!of a set}
 Note that it is denoted by a minus sign.
 \begin{isabelle}
 (c\ \isasymin\ -\ A)\ =\ (c\ \isasymnotin\ A)
@@ -745,7 +745,7 @@
 The \textbf{reflexive and transitive closure} of the
 relation~\isa{r} is written with a
 postfix syntax.  In ASCII we write \isa{r\isacharcircum*} and in
-X-symbol notation~\isa{r\isactrlsup *}.  It is the least solution of the
+symbol notation~\isa{r\isactrlsup *}.  It is the least solution of the
 equation
 \begin{isabelle}
 r\isactrlsup *\ =\ Id\ \isasymunion \ (r\ O\ r\isactrlsup *)

--- a/doc-src/TutorialI/Types/Axioms.thy	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Types/Axioms.thy	Fri Jan 18 18:30:19 2002 +0100
@@ -54,7 +54,7 @@
 when the proposition is not a theorem.  The proof is easy:
 *}
 
-by(simp add:less_le antisym);
+by(simp add: less_le antisym);
 
 text{* We could now continue in this vein and develop a whole theory of
 results about partial orders. Eventually we will want to apply these results
@@ -147,7 +147,7 @@
 are easily proved:
 *}
 
-  apply(simp_all (no_asm_use) add:less_le);
+  apply(simp_all (no_asm_use) add: less_le);
  apply(blast intro: trans antisym);
 apply(blast intro: refl);
 done
@@ -161,7 +161,7 @@
 (*
 instance strord < parord
 apply intro_classes;
-apply(simp_all (no_asm_use) add:le_less);
+apply(simp_all (no_asm_use) add: le_less);
 apply(blast intro: less_trans);
 apply(erule disjE);
 apply(erule disjE);
@@ -193,7 +193,7 @@
 \begin{figure}[htbp]
 \[
 \begin{array}{r@ {}r@ {}c@ {}l@ {}l}
-& & \isa{term}\\
+& & \isa{type}\\
 & & |\\
 & & \isa{ordrel}\\
 & & |\\

--- a/doc-src/TutorialI/Types/Overloading1.thy	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Types/Overloading1.thy	Fri Jan 18 18:30:19 2002 +0100
@@ -5,7 +5,7 @@
 text{*
 We now start with the theory of ordering relations, which we shall phrase
 in terms of the two binary symbols @{text"<<"} and @{text"<<="}
-to avoid clashes with @{text"<"} and @{text"\<le>"} in theory @{text
+to avoid clashes with @{text"<"} and @{text"<="} in theory @{text
 Main}. To restrict the application of @{text"<<"} and @{text"<<="} we
 introduce the class @{text ordrel}:
 *}

--- a/doc-src/TutorialI/Types/Pairs.thy	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Types/Pairs.thy	Fri Jan 18 18:30:19 2002 +0100
@@ -55,7 +55,7 @@
 *}
 
 lemma "(\<lambda>(x,y).x) p = fst p"
-by(simp add:split_def)
+by(simp add: split_def)
 
 text{* This works well if rewriting with @{thm[source]split_def} finishes the
 proof, as it does above.  But if it does not, you end up with exactly what
@@ -102,7 +102,7 @@
 can be split as above. The same is true for paired set comprehension:
 *}
 
-(*<*)by(simp split:split_split)(*>*)
+(*<*)by(simp split: split_split)(*>*)
 lemma "p \<in> {(x,y). x=y} \<longrightarrow> fst p = snd p"
 apply simp
 
@@ -114,7 +114,7 @@
 The same proof procedure works for
 *}
 
-(*<*)by(simp split:split_split)(*>*)
+(*<*)by(simp split: split_split)(*>*)
 lemma "p \<in> {(x,y). x=y} \<Longrightarrow> fst p = snd p"
 
 txt{*\noindent
@@ -125,7 +125,7 @@
 may be present in the goal. Consider the following function:
 *}
 
-(*<*)by(simp split:split_split_asm)(*>*)
+(*<*)by(simp split: split_split_asm)(*>*)
 consts swap :: "'a \<times> 'b \<Rightarrow> 'b \<times> 'a"
 primrec
   "swap (x,y) = (y,x)"
@@ -184,7 +184,7 @@
 (*<*)
 lemma "\<And>p q. swap(swap p) = q \<longrightarrow> p = q"
 (*>*)
-apply(simp add:split_paired_all)
+apply(simp add: split_paired_all)
 (*<*)done(*>*)
 text{*\noindent
 Finally, the simplifier automatically splits all @{text"\<forall>"} and

--- a/doc-src/TutorialI/Types/Typedefs.thy	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Types/Typedefs.thy	Fri Jan 18 18:30:19 2002 +0100
@@ -195,7 +195,7 @@
 
 txt{*\noindent Again this follows easily from a pre-proved general theorem:*}
 
-apply(rule_tac x = x in Abs_three_induct)
+apply(induct_tac x rule: Abs_three_induct)
 
 txt{*
 @{subgoals[display,indent=0]}

--- a/doc-src/TutorialI/Types/document/Axioms.tex	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Types/document/Axioms.tex	Fri Jan 18 18:30:19 2002 +0100
@@ -64,7 +64,7 @@
 when the proposition is not a theorem.  The proof is easy:%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}less{\isacharunderscore}le\ antisym{\isacharparenright}\isamarkupfalse%
+\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ less{\isacharunderscore}le\ antisym{\isacharparenright}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 We could now continue in this vein and develop a whole theory of
@@ -193,7 +193,7 @@
 are easily proved:%
 \end{isamarkuptxt}%
 \ \ \isamarkuptrue%
-\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}\ add{\isacharcolon}less{\isacharunderscore}le{\isacharparenright}\isanewline
+\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}\ add{\isacharcolon}\ less{\isacharunderscore}le{\isacharparenright}\isanewline
 \ \isamarkupfalse%
 \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ trans\ antisym{\isacharparenright}\isanewline
 \isamarkupfalse%
@@ -232,7 +232,7 @@
 \begin{figure}[htbp]
 \[
 \begin{array}{r@ {}r@ {}c@ {}l@ {}l}
-& & \isa{term}\\
+& & \isa{type}\\
 & & |\\
 & & \isa{ordrel}\\
 & & |\\

--- a/doc-src/TutorialI/Types/document/Overloading1.tex	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading1.tex	Fri Jan 18 18:30:19 2002 +0100
@@ -10,7 +10,7 @@
 \begin{isamarkuptext}%
 We now start with the theory of ordering relations, which we shall phrase
 in terms of the two binary symbols \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}}
-to avoid clashes with \isa{{\isacharless}} and \isa{{\isasymle}} in theory \isa{Main}. To restrict the application of \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} we
+to avoid clashes with \isa{{\isacharless}} and \isa{{\isacharless}{\isacharequal}} in theory \isa{Main}. To restrict the application of \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} we
 introduce the class \isa{ordrel}:%
 \end{isamarkuptext}%
 \isamarkuptrue%

--- a/doc-src/TutorialI/Types/document/Pairs.tex	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Types/document/Pairs.tex	Fri Jan 18 18:30:19 2002 +0100
@@ -67,7 +67,7 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}x{\isacharparenright}\ p\ {\isacharequal}\ fst\ p{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}split{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
+\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ split{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 This works well if rewriting with \isa{split{\isacharunderscore}def} finishes the
@@ -218,7 +218,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}\isamarkupfalse%
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%

--- a/doc-src/TutorialI/Types/document/Typedefs.tex	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Types/document/Typedefs.tex	Fri Jan 18 18:30:19 2002 +0100
@@ -218,7 +218,7 @@
 \noindent Again this follows easily from a pre-proved general theorem:%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ x\ \isakeyword{in}\ Abs{\isacharunderscore}three{\isacharunderscore}induct{\isacharparenright}\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ x\ rule{\isacharcolon}\ Abs{\isacharunderscore}three{\isacharunderscore}induct{\isacharparenright}\isamarkupfalse%
 %
 \begin{isamarkuptxt}%
 \begin{isabelle}%