src/HOL/Library/Primes.thy

   apply simp
   done
 
 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
 
 text {*
   \medskip @{term "gcd (m, n)"} divides @{text m} and @{text n}.  The

 
 lemma gcd_0_left [simp]: "gcd (0, m) = m"
   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
 
 
 text {*
   \medskip Multiplication laws

 
 lemma prime_dvd_mult: "p \<in> prime ==> p dvd m * n ==> p dvd m \<or> p dvd n"
   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
 
 
 text {* \medskip Addition laws *}