src/HOL/GCD.thy
changeset 32415 1dddf2f64266
parent 32112 6da9c2a49fed
child 32479 521cc9bf2958
     1.1 --- a/src/HOL/GCD.thy	Wed Aug 26 16:41:37 2009 +0200
     1.2 +++ b/src/HOL/GCD.thy	Wed Aug 26 19:54:01 2009 +0200
     1.3 @@ -1895,8 +1895,6 @@
     1.4  
     1.5  lemmas prime_int_simp_number_of[simp] = prime_int_simp[of "number_of m", standard]
     1.6  
     1.7 -declare successor_int_def[simp]
     1.8 -
     1.9  lemma two_is_prime_nat [simp]: "prime (2::nat)"
    1.10  by simp
    1.11