| changeset 5228 | 66925577cefe |
| parent 5185 | d1067e2c3f9f |
| child 5299 | d15a4155b96b |
--- a/src/HOL/HOL.ML Fri Jul 31 11:03:21 1998 +0200 +++ b/src/HOL/HOL.ML Fri Jul 31 11:03:31 1998 +0200 @@ -251,9 +251,9 @@ [rtac (major RS exE) 1, REPEAT (etac conjE 1 ORELSE ares_tac prems 1)]); Goal "?! x. P x ==> ? x. P x"; -be ex1E 1; -br exI 1; -ba 1; +by (etac ex1E 1); +by (rtac exI 1); +by (assume_tac 1); qed "ex1_implies_ex";