diff -r 3c50a2cd6f00 -r ac8ca15c556c doc-src/TutorialI/Inductive/Even.thy
--- a/doc-src/TutorialI/Inductive/Even.thy	Sat Oct 06 00:02:46 2001 +0200
+++ b/doc-src/TutorialI/Inductive/Even.thy	Mon Oct 08 12:13:34 2001 +0200
@@ -20,7 +20,7 @@
 specified as \isa{intro!}
 
 Our first lemma states that numbers of the form $2\times k$ are even. *}
-lemma two_times_even[intro!]: "#2*k \<in> even"
+lemma two_times_even[intro!]: "2*k \<in> even"
 apply (induct "k")
 txt{*
 The first step is induction on the natural number \isa{k}, which leaves
@@ -36,11 +36,11 @@
 this equivalence is trivial using the lemma just proved, whose \isa{intro!}
 attribute ensures it will be applied automatically.  *}
 
-lemma dvd_imp_even: "#2 dvd n \<Longrightarrow> n \<in> even"
+lemma dvd_imp_even: "2 dvd n \<Longrightarrow> n \<in> even"
 by (auto simp add: dvd_def)
 
 text{*our first rule induction!*}
-lemma even_imp_dvd: "n \<in> even \<Longrightarrow> #2 dvd n"
+lemma even_imp_dvd: "n \<in> even \<Longrightarrow> 2 dvd n"
 apply (erule even.induct)
 txt{*
 @{subgoals[display,indent=0,margin=65]}
@@ -58,7 +58,7 @@
 
 
 text{*no iff-attribute because we don't always want to use it*}
-theorem even_iff_dvd: "(n \<in> even) = (#2 dvd n)"
+theorem even_iff_dvd: "(n \<in> even) = (2 dvd n)"
 by (blast intro: dvd_imp_even even_imp_dvd)
 
 text{*this result ISN'T inductive...*}
@@ -70,7 +70,7 @@
 oops
 
 text{*...so we need an inductive lemma...*}
-lemma even_imp_even_minus_2: "n \<in> even \<Longrightarrow> n-#2 \<in> even"
+lemma even_imp_even_minus_2: "n \<in> even \<Longrightarrow> n - 2 \<in> even"
 apply (erule even.induct)
 txt{*
 @{subgoals[display,indent=0,margin=65]}