equal
deleted
inserted
replaced
4 Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4 |
4 Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4 |
5 *) |
5 *) |
6 |
6 |
7 header{*Exponentials on the Hyperreals*} |
7 header{*Exponentials on the Hyperreals*} |
8 |
8 |
9 theory HyperPow = HyperArith + HyperNat + "../Real/RealPow": |
9 theory HyperPow |
|
10 import HyperArith HyperNat "../Real/RealPow" |
|
11 begin |
10 |
12 |
11 instance hypreal :: power .. |
13 instance hypreal :: power .. |
12 |
14 |
13 consts hpowr :: "[hypreal,nat] => hypreal" |
15 consts hpowr :: "[hypreal,nat] => hypreal" |
14 primrec |
16 primrec |