| changeset 66453 | cc19f7ca2ed6 |
| parent 66280 | 0c5eb47e2696 |
| child 67573 | ed0a7090167d |
| 66452:450cefec7c11 | 66453:cc19f7ca2ed6 |
|---|---|
9 *) |
9 *) |
10 |
10 |
11 theory Approximation_Bounds |
11 theory Approximation_Bounds |
12 imports |
12 imports |
13 Complex_Main |
13 Complex_Main |
14 "~~/src/HOL/Library/Float" |
14 "HOL-Library.Float" |
15 Dense_Linear_Order |
15 Dense_Linear_Order |
16 begin |
16 begin |
17 |
17 |
18 declare powr_neg_one [simp] |
18 declare powr_neg_one [simp] |
19 declare powr_neg_numeral [simp] |
19 declare powr_neg_numeral [simp] |