| changeset 10171 | 59d6633835fa |
| parent 9792 | bbefb6ce5cb2 |
| child 10362 | c6b197ccf1f1 |
--- a/doc-src/TutorialI/Recdef/Induction.thy Mon Oct 09 09:33:45 2000 +0200 +++ b/doc-src/TutorialI/Recdef/Induction.thy Mon Oct 09 10:18:21 2000 +0200 @@ -41,7 +41,8 @@ The rest is pure simplification: *} -by simp_all; +apply simp_all; +done text{* Try proving the above lemma by structural induction, and you find that you