--- a/src/HOL/Complex/ex/NSPrimes.thy Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Complex/ex/NSPrimes.thy Fri Nov 17 02:20:03 2006 +0100
@@ -14,13 +14,15 @@
primes by considering a property of nonstandard sets.*}
definition
- hdvd :: "[hypnat, hypnat] => bool" (infixl "hdvd" 50)
+ hdvd :: "[hypnat, hypnat] => bool" (infixl "hdvd" 50) where
[transfer_unfold]: "(M::hypnat) hdvd N = ( *p2* (op dvd)) M N"
- starprime :: "hypnat set"
+definition
+ starprime :: "hypnat set" where
[transfer_unfold]: "starprime = ( *s* {p. prime p})"
- choicefun :: "'a set => 'a"
+definition
+ choicefun :: "'a set => 'a" where
"choicefun E = (@x. \<exists>X \<in> Pow(E) -{{}}. x : X)"
consts injf_max :: "nat => ('a::{order} set) => 'a"