Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
isatool expandshort;
authorwenzelm
Fri, 31 Jul 1998 11:03:31 +0200
changeset 5228 66925577cefe
parent 5227 e5a6ace920a0
child 5229 7c8abffc4413
isatool expandshort;
src/HOL/HOL.ML file | annotate | diff | comparison | revisions 
--- 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";
isabelle