--- a/src/HOL/GCD.thy Wed Jun 17 18:27:04 2009 -0700
+++ b/src/HOL/GCD.thy Thu Jun 18 07:46:30 2009 -0700
@@ -83,7 +83,7 @@
definition
prime_nat :: "nat \<Rightarrow> bool"
where
- "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
+ [code del]: "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
instance proof qed
@@ -118,7 +118,7 @@
definition
prime_int :: "int \<Rightarrow> bool"
where
- "prime_int p = prime (nat p)"
+ [code del]: "prime_int p = prime (nat p)"
instance proof qed