equal
deleted
inserted
replaced
12 uses ("fuf.ML") (*Warning: file fuf.ML refers to the name Hyperdef!*) |
12 uses ("fuf.ML") (*Warning: file fuf.ML refers to the name Hyperdef!*) |
13 begin |
13 begin |
14 |
14 |
15 types hypreal = "real star" |
15 types hypreal = "real star" |
16 |
16 |
17 syntax hypreal_of_real :: "real => real star" |
17 abbreviation |
18 translations "hypreal_of_real" => "star_of :: real => real star" |
18 hypreal_of_real :: "real => real star" |
|
19 "hypreal_of_real == star_of" |
19 |
20 |
20 constdefs |
21 constdefs |
21 |
22 |
22 omega :: hypreal -- {*an infinite number @{text "= [<1,2,3,...>]"} *} |
23 omega :: hypreal -- {*an infinite number @{text "= [<1,2,3,...>]"} *} |
23 "omega == star_n (%n. real (Suc n))" |
24 "omega == star_n (%n. real (Suc n))" |