# HG changeset patch
# User Andreas Lochbihler
# Date 1426165727 -3600
# Node ID 034a4d15b52eb284baf4d4dac12bc3726632f9a1
# Parent  2574977f9afa0993e9b185305d7dc8fdbe03da87
make proofs work with 4762c690a75c

diff -r 2574977f9afa -r 034a4d15b52e src/HOL/NSA/Examples/NSPrimes.thy
--- 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})"
diff -r 2574977f9afa -r 034a4d15b52e src/HOL/NSA/StarDef.thy
--- 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