| changeset 13601 | fd3e3d6b37b2 |
| parent 12486 | 0ed8bdd883e0 |
| child 14265 | 95b42e69436c |
--- a/src/HOL/Hyperreal/NthRoot.ML Mon Sep 30 16:12:16 2002 +0200 +++ b/src/HOL/Hyperreal/NthRoot.ML Mon Sep 30 16:14:02 2002 +0200 @@ -30,7 +30,8 @@ by (dtac not_real_leE 2); by (res_inst_tac [("x","1")] exI 2); by (ALLGOALS(rtac (setleI RS isUbI))); -by (Auto_tac); +by Safe_tac; +by (ALLGOALS Simp_tac); by (ALLGOALS(rtac ccontr)); by (ALLGOALS(dtac not_real_leE)); by (dtac realpow_ge_self2 1 THEN assume_tac 1);