src/HOL/Library/Primes.thy
changeset 11701 3d51fbf81c17
parent 11464 ddea204de5bc
child 12300 9fbce4042034
     1.1 --- a/src/HOL/Library/Primes.thy	Fri Oct 05 21:50:37 2001 +0200
     1.2 +++ b/src/HOL/Library/Primes.thy	Fri Oct 05 21:52:39 2001 +0200
     1.3 @@ -54,7 +54,7 @@
     1.4  
     1.5  declare gcd.simps [simp del]
     1.6  
     1.7 -lemma gcd_1 [simp]: "gcd (m, 1') = 1"
     1.8 +lemma gcd_1 [simp]: "gcd (m, Suc 0) = 1"
     1.9    apply (simp add: gcd_non_0)
    1.10    done
    1.11  
    1.12 @@ -140,8 +140,8 @@
    1.13    apply (simp add: gcd_commute [of 0])
    1.14    done
    1.15  
    1.16 -lemma gcd_1_left [simp]: "gcd (1', m) = 1"
    1.17 -  apply (simp add: gcd_commute [of "1'"])
    1.18 +lemma gcd_1_left [simp]: "gcd (Suc 0, m) = 1"
    1.19 +  apply (simp add: gcd_commute [of "Suc 0"])
    1.20    done
    1.21  
    1.22  
    1.23 @@ -194,7 +194,7 @@
    1.24    apply (blast intro: relprime_dvd_mult prime_imp_relprime)
    1.25    done
    1.26  
    1.27 -lemma prime_dvd_square: "p \<in> prime ==> p dvd m^2 ==> p dvd m"
    1.28 +lemma prime_dvd_square: "p \<in> prime ==> p dvd m^Suc (Suc 0) ==> p dvd m"
    1.29    apply (auto dest: prime_dvd_mult)
    1.30    done
    1.31