| changeset 8442 | 96023903c2df |
| parent 8423 | 3c19160b6432 |
| child 8838 | 4eaa99f0d223 |
--- a/src/HOL/Real/RealPow.ML Mon Mar 13 15:42:19 2000 +0100 +++ b/src/HOL/Real/RealPow.ML Mon Mar 13 16:23:34 2000 +0100 @@ -234,7 +234,7 @@ qed_spec_mp "realpow_Suc_le"; Goal "0r <= 0r ^ n"; -by (cases_tac "n" 1); +by (case_tac "n" 1); by (Auto_tac); qed "realpow_zero_le"; Addsimps [realpow_zero_le];