| changeset 10699 | f0c3da8477e9 |
| parent 10690 | cd80241125b0 |
| child 10712 | 351ba950d4d9 |
--- a/src/HOL/Real/RealPow.ML Tue Dec 19 15:06:14 2000 +0100 +++ b/src/HOL/Real/RealPow.ML Tue Dec 19 15:06:59 2000 +0100 @@ -143,7 +143,6 @@ by (auto_tac (claset() addSDs [real_le_imp_less_or_eq], simpset())); by (dtac (rename_numerals (real_zero_less_one RS real_mult_less_mono)) 1); -by (dtac sym 4); by (auto_tac (claset() addSIs [real_less_imp_le], simpset() addsimps [real_zero_less_one])); qed_spec_mp "realpow_ge_one";