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