--- a/src/ZF/Arith.thy Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/Arith.thy Thu Jan 23 10:30:14 2003 +0100
@@ -200,7 +200,7 @@
(*Must simplify BEFORE the induction: else we get a critical pair*)
lemma diff_succ_succ [simp]: "succ(m) #- succ(n) = m #- n"
apply (simp add: natify_succ diff_def)
-apply (rule_tac x1 = "n" in natify_in_nat [THEN nat_induct], auto)
+apply (rule_tac x1 = n in natify_in_nat [THEN nat_induct], auto)
done
(*This defining property is no longer wanted*)
@@ -212,7 +212,7 @@
lemma diff_le_self: "m:nat ==> (m #- n) le m"
apply (subgoal_tac " (m #- natify (n)) le m")
-apply (rule_tac [2] m = "m" and n = "natify (n) " in diff_induct)
+apply (rule_tac [2] m = m and n = "natify (n) " in diff_induct)
apply (erule_tac [6] leE)
apply (simp_all add: le_iff)
done
@@ -528,7 +528,7 @@
lemma less_diff_conv [rule_format]:
"[| j:nat; k:nat |] ==> ALL i:nat. (i < j #- k) <-> (i #+ k < j)"
-by (erule_tac m = "k" in diff_induct, auto)
+by (erule_tac m = k in diff_induct, auto)
lemmas nat_typechecks = rec_type nat_0I nat_1I nat_succI Ord_nat