| changeset 15140 | 322485b816ac |
| parent 15131 | c69542757a4d |
| child 16417 | 9bc16273c2d4 |
| 15139:58cd3404cf75 | 15140:322485b816ac |
|---|---|
5 *) |
5 *) |
6 |
6 |
7 header{*Binary arithmetic and Simplification for the Hyperreals*} |
7 header{*Binary arithmetic and Simplification for the Hyperreals*} |
8 |
8 |
9 theory HyperArith |
9 theory HyperArith |
10 import HyperDef |
10 imports HyperDef |
11 files ("hypreal_arith.ML") |
11 files ("hypreal_arith.ML") |
12 begin |
12 begin |
13 |
13 |
14 subsection{*Numerals and Arithmetic*} |
14 subsection{*Numerals and Arithmetic*} |
15 |
15 |