--- a/src/HOL/NSA/Examples/NSPrimes.thy Wed Mar 11 11:21:58 2015 +0100
+++ b/src/HOL/NSA/Examples/NSPrimes.thy Thu Mar 12 14:08:47 2015 +0100
@@ -13,8 +13,6 @@
text{*These can be used to derive an alternative proof of the infinitude of
primes by considering a property of nonstandard sets.*}
-declare dvd_def [transfer_refold]
-
definition
starprime :: "hypnat set" where
[transfer_unfold]: "starprime = ( *s* {p. prime p})"
--- a/src/HOL/NSA/StarDef.thy Wed Mar 11 11:21:58 2015 +0100
+++ b/src/HOL/NSA/StarDef.thy Thu Mar 12 14:08:47 2015 +0100
@@ -848,11 +848,7 @@
instance star :: (semiring_1) semiring_1 ..
instance star :: (comm_semiring_1) comm_semiring_1 ..
-lemma star_dvd_def [transfer_unfold]: "op dvd = *p2* (op dvd)"
-apply (rule ext)+
-apply (unfold dvd_def[abs_def], transfer)
-apply (rule refl)
-done
+declare dvd_def [transfer_refold]
instance star :: (semiring_dvd) semiring_dvd
apply intro_classes