diff -r 2f5edb146f7e -r 1f073030b97a doc-src/TutorialI/Inductive/AB.thy
--- 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