| changeset 9458 | c613cd06d5cf |
| parent 8771 | 026f37a86ea7 |
| child 9541 | d17c0b34d5c8 |
--- a/doc-src/TutorialI/Misc/case_splits.thy Fri Jul 28 13:04:59 2000 +0200 +++ b/doc-src/TutorialI/Misc/case_splits.thy Fri Jul 28 16:02:51 2000 +0200 @@ -53,7 +53,7 @@ (*<*) lemma "(case xs of [] \\<Rightarrow> zs | y#ys \\<Rightarrow> y#(ys@zs)) = xs@zs"; (*>*) -apply(simp split: list.split).; +by(simp split: list.split); text{*\noindent% which \isacommand{apply}\isa{(simp)} alone will not do.