more [code del] declarations
authorhuffman
Thu Jun 18 07:46:30 2009 -0700 (2009-06-18)
changeset 31709061f01ee9978
parent 31708 a3fce678c320
child 31710 99f08ce977f9
more [code del] declarations
src/HOL/GCD.thy
     1.1 --- a/src/HOL/GCD.thy	Wed Jun 17 18:27:04 2009 -0700
     1.2 +++ b/src/HOL/GCD.thy	Thu Jun 18 07:46:30 2009 -0700
     1.3 @@ -83,7 +83,7 @@
     1.4  definition
     1.5    prime_nat :: "nat \<Rightarrow> bool"
     1.6  where
     1.7 -  "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
     1.8 +  [code del]: "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 @@ -118,7 +118,7 @@
    1.13  definition
    1.14    prime_int :: "int \<Rightarrow> bool"
    1.15  where
    1.16 -  "prime_int p = prime (nat p)"
    1.17 +  [code del]: "prime_int p = prime (nat p)"
    1.18  
    1.19  instance proof qed
    1.20