changeset 15140 | 322485b816ac |
parent 15131 | c69542757a4d |
child 15169 | 2b5da07a0b89 |
15139:58cd3404cf75 | 15140:322485b816ac |
---|---|
6 *) |
6 *) |
7 |
7 |
8 header{*Star-transforms for the Hypernaturals*} |
8 header{*Star-transforms for the Hypernaturals*} |
9 |
9 |
10 theory NatStar |
10 theory NatStar |
11 import "../Real/RealPow" HyperPow |
11 imports "../Real/RealPow" HyperPow |
12 begin |
12 begin |
13 |
13 |
14 text{*Extends sets of nats, and functions from the nats to nats or reals*} |
14 text{*Extends sets of nats, and functions from the nats to nats or reals*} |
15 |
15 |
16 |
16 |