--- a/src/HOL/Real/Hyperreal/HyperDef.thy Fri Dec 01 19:42:05 2000 +0100 +++ b/src/HOL/Real/Hyperreal/HyperDef.thy Fri Dec 01 19:42:35 2000 +0100 @@ -9,7 +9,7 @@ consts - FreeUltrafilterNat :: nat set set + FreeUltrafilterNat :: nat set set ("\\<U>") defs