| changeset 12815 | 1f073030b97a |
| parent 11293 | 6878bb02a7f9 |
| child 13238 | a6cb18a25cbb |
--- 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{*