changeset 14361 | ad2f5da643b4 |
parent 14348 | 744c868ee0b7 |
child 14365 | 3d4df8c166ae |
--- a/src/HOL/Hyperreal/HyperDef.thy Sun Jan 25 00:42:22 2004 +0100 +++ b/src/HOL/Hyperreal/HyperDef.thy Mon Jan 26 10:34:02 2004 +0100 @@ -11,7 +11,7 @@ constdefs - FreeUltrafilterNat :: "nat set set" ("\\<U>") + FreeUltrafilterNat :: "nat set set" ("\<U>") "FreeUltrafilterNat == (SOME U. U \<in> FreeUltrafilter (UNIV:: nat set))" hyprel :: "((nat=>real)*(nat=>real)) set"