--- a/doc-src/TutorialI/Misc/asm_simp.thy Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/asm_simp.thy Fri Jul 28 16:02:51 2000 +0200
@@ -7,7 +7,7 @@
*}
lemma "\\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \\<rbrakk> \\<Longrightarrow> ys = zs";
-apply simp.;
+by simp;
text{*\noindent
The second assumption simplifies to \isa{xs = []}, which in turn
@@ -28,7 +28,7 @@
explicitly telling the simplifier to ignore the assumptions:
*}
-apply(simp (no_asm)).;
+by(simp (no_asm));
text{*\noindent
There are three options that influence the treatment of assumptions: