equal
deleted
inserted
replaced
5 Converted to Isar and polished by lcp |
5 Converted to Isar and polished by lcp |
6 *) |
6 *) |
7 |
7 |
8 header{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*} |
8 header{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*} |
9 |
9 |
10 theory NSA = HyperArith + RComplete: |
10 theory NSA |
|
11 import HyperArith RComplete |
|
12 begin |
11 |
13 |
12 constdefs |
14 constdefs |
13 |
15 |
14 Infinitesimal :: "hypreal set" |
16 Infinitesimal :: "hypreal set" |
15 "Infinitesimal == {x. \<forall>r \<in> Reals. 0 < r --> abs x < r}" |
17 "Infinitesimal == {x. \<forall>r \<in> Reals. 0 < r --> abs x < r}" |