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.
tuned;
authorwenzelm
Fri, 20 Jul 2001 21:53:27 +0200
changeset 11433 cf7dae62d69d
parent 11432 8a203ae6efe3
child 11434 996bd4eb0ef3
tuned;
src/HOL/HOL_lemmas.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/HOL_lemmas.ML	Fri Jul 20 21:52:54 2001 +0200
+++ b/src/HOL/HOL_lemmas.ML	Fri Jul 20 21:53:27 2001 +0200
@@ -421,7 +421,7 @@
 by (REPEAT (ares_tac [prema,premx] 1));
 qed "theI";
 
-Goal "(EX! x. P x) ==> P (THE x. P x)";
+Goal "EX! x. P x ==> P (THE x. P x)";
 by (etac ex1E 1);
 by (etac theI 1);
 by (etac allE 1);
isabelle