src/HOL/Number_Theory/Primes.thy
changeset 37765 26bdfb7b680b
parent 37607 ebb8b1a79c4c
child 40461 e876e95588ce
     1.1 --- a/src/HOL/Number_Theory/Primes.thy	Mon Jul 12 08:58:12 2010 +0200
     1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Mon Jul 12 08:58:13 2010 +0200
     1.3 @@ -45,7 +45,7 @@
     1.4  definition
     1.5    prime_nat :: "nat \<Rightarrow> bool"
     1.6  where
     1.7 -  [code del]: "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
     1.8 +  "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
     1.9  
    1.10  instance proof qed
    1.11  
    1.12 @@ -58,7 +58,7 @@
    1.13  definition
    1.14    prime_int :: "int \<Rightarrow> bool"
    1.15  where
    1.16 -  [code del]: "prime_int p = prime (nat p)"
    1.17 +  "prime_int p = prime (nat p)"
    1.18  
    1.19  instance proof qed
    1.20