| changeset 9458 | c613cd06d5cf |
| parent 8771 | 026f37a86ea7 |
| child 9541 | d17c0b34d5c8 |
--- a/doc-src/TutorialI/Misc/let_rewr.thy Fri Jul 28 13:04:59 2000 +0200 +++ b/doc-src/TutorialI/Misc/let_rewr.thy Fri Jul 28 16:02:51 2000 +0200 @@ -2,7 +2,7 @@ theory let_rewr = Main:; (*>*) lemma "(let xs = [] in xs@ys@xs) = ys"; -apply(simp add: Let_def).; +by(simp add: Let_def); text{* If, in a particular context, there is no danger of a combinatorial explosion