--- 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