| changeset 15140 | 322485b816ac |
| parent 15131 | c69542757a4d |
| child 15229 | 1eb23f805c06 |
| 15139:58cd3404cf75 | 15140:322485b816ac |
|---|---|
5 Description : Natural powers theory |
5 Description : Natural powers theory |
6 |
6 |
7 *) |
7 *) |
8 |
8 |
9 theory RealPow |
9 theory RealPow |
10 import RealDef |
10 imports RealDef |
11 begin |
11 begin |
12 |
12 |
13 declare abs_mult_self [simp] |
13 declare abs_mult_self [simp] |
14 |
14 |
15 instance real :: power .. |
15 instance real :: power .. |