| changeset 16417 | 9bc16273c2d4 |
| parent 15140 | 322485b816ac |
| child 16924 | 04246269386e |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
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 imports HyperDef |
10 imports HyperDef |
11 files ("hypreal_arith.ML") |
11 uses ("hypreal_arith.ML") |
12 begin |
12 begin |
13 |
13 |
14 subsection{*Numerals and Arithmetic*} |
14 subsection{*Numerals and Arithmetic*} |
15 |
15 |
16 instance hypreal :: number .. |
16 instance hypreal :: number .. |