# HG changeset patch
# User huffman
# Date 1245336390 25200
# Node ID 061f01ee9978a8fc5c8dbb44db40c69c28561d13
# Parent  a3fce678c3203d14504a30ca22c976fcd63979d8
more [code del] declarations

diff -r a3fce678c320 -r 061f01ee9978 src/HOL/GCD.thy
--- 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