--- a/doc-src/TutorialI/Misc/cond_rewr.thy Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/cond_rewr.thy Fri Jul 28 16:02:51 2000 +0200
@@ -8,7 +8,7 @@
*}
lemma hd_Cons_tl[simp]: "xs \\<noteq> [] \\<Longrightarrow> hd xs # tl xs = xs";
-apply(case_tac xs, simp, simp).;
+by(case_tac xs, simp, simp);
text{*\noindent
Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a
@@ -20,7 +20,7 @@
lemma "xs \\<noteq> [] \\<Longrightarrow> hd(rev xs) # tl(rev xs) = rev xs";
(*<*)
-apply(simp).
+by(simp);
(*>*)
text{*\noindent
is proved by plain simplification: