src/HOL/Real/Hyperreal/HyperDef.thy
changeset 10568 a7701b1d6c6a
parent 9391 a6ab3a442da6
child 10607 352f6f209775
equal deleted inserted replaced
10567:e7c9900cca4d 10568:a7701b1d6c6a
     7 
     7 
     8 HyperDef = Filter + Real +
     8 HyperDef = Filter + Real +
     9 
     9 
    10 consts 
    10 consts 
    11  
    11  
    12     FreeUltrafilterNat   :: nat set set
    12     FreeUltrafilterNat   :: nat set set    ("\\<U>")
    13 
    13 
    14 defs
    14 defs
    15 
    15 
    16     FreeUltrafilterNat_def
    16     FreeUltrafilterNat_def
    17     "FreeUltrafilterNat    ==   (@U. U : FreeUltrafilter (UNIV:: nat set))"
    17     "FreeUltrafilterNat    ==   (@U. U : FreeUltrafilter (UNIV:: nat set))"