--- a/src/HOL/Library/Primes.thy Fri Oct 05 21:50:37 2001 +0200
+++ b/src/HOL/Library/Primes.thy Fri Oct 05 21:52:39 2001 +0200
@@ -54,7 +54,7 @@
declare gcd.simps [simp del]
-lemma gcd_1 [simp]: "gcd (m, 1') = 1"
+lemma gcd_1 [simp]: "gcd (m, Suc 0) = 1"
apply (simp add: gcd_non_0)
done
@@ -140,8 +140,8 @@
apply (simp add: gcd_commute [of 0])
done
-lemma gcd_1_left [simp]: "gcd (1', m) = 1"
- apply (simp add: gcd_commute [of "1'"])
+lemma gcd_1_left [simp]: "gcd (Suc 0, m) = 1"
+ apply (simp add: gcd_commute [of "Suc 0"])
done
@@ -194,7 +194,7 @@
apply (blast intro: relprime_dvd_mult prime_imp_relprime)
done
-lemma prime_dvd_square: "p \<in> prime ==> p dvd m^2 ==> p dvd m"
+lemma prime_dvd_square: "p \<in> prime ==> p dvd m^Suc (Suc 0) ==> p dvd m"
apply (auto dest: prime_dvd_mult)
done