| changeset 9458 | c613cd06d5cf |
| parent 8771 | 026f37a86ea7 |
| child 9689 | 751fde5307e4 |
--- a/doc-src/TutorialI/Recdef/Induction.thy Fri Jul 28 13:04:59 2000 +0200 +++ b/doc-src/TutorialI/Recdef/Induction.thy Fri Jul 28 16:02:51 2000 +0200 @@ -41,7 +41,7 @@ The rest is pure simplification: *} -apply auto.; +by auto; text{* Try proving the above lemma by structural induction, and you find that you