13 begin |
13 begin |
14 |
14 |
15 types hypreal = "real star" |
15 types hypreal = "real star" |
16 |
16 |
17 abbreviation |
17 abbreviation |
18 hypreal_of_real :: "real => real star" |
18 hypreal_of_real :: "real => real star" where |
19 "hypreal_of_real == star_of" |
19 "hypreal_of_real == star_of" |
20 |
20 |
21 definition |
21 definition |
22 omega :: hypreal -- {*an infinite number @{text "= [<1,2,3,...>]"} *} |
22 omega :: hypreal where -- {*an infinite number @{text "= [<1,2,3,...>]"} *} |
23 "omega = star_n (%n. real (Suc n))" |
23 "omega = star_n (%n. real (Suc n))" |
24 |
24 |
25 epsilon :: hypreal -- {*an infinitesimal number @{text "= [<1,1/2,1/3,...>]"} *} |
25 definition |
|
26 epsilon :: hypreal where -- {*an infinitesimal number @{text "= [<1,1/2,1/3,...>]"} *} |
26 "epsilon = star_n (%n. inverse (real (Suc n)))" |
27 "epsilon = star_n (%n. inverse (real (Suc n)))" |
27 |
28 |
28 notation (xsymbols) |
29 notation (xsymbols) |
29 omega ("\<omega>") |
30 omega ("\<omega>") and |
30 epsilon ("\<epsilon>") |
31 epsilon ("\<epsilon>") |
31 |
32 |
32 notation (HTML output) |
33 notation (HTML output) |
33 omega ("\<omega>") |
34 omega ("\<omega>") and |
34 epsilon ("\<epsilon>") |
35 epsilon ("\<epsilon>") |
35 |
36 |
36 |
37 |
37 subsection {* Real vector class instances *} |
38 subsection {* Real vector class instances *} |
38 |
39 |