Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/cladata.ML
changeset 3842 b55686a7b22c
parent 3615 e5322197cfea
child 4059 59c1422c9da5 
--- a/src/HOL/cladata.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/cladata.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -68,7 +68,7 @@
 
 (*Better then ex1E for classical reasoner: needs no quantifier duplication!*)
 qed_goal "alt_ex1E" thy
-    "[| ?! x.P(x);                                              \
+    "[| ?! x. P(x);                                              \
 \       !!x. [| P(x);  ALL y y'. P(y) & P(y') --> y=y' |] ==> R  \
 \    |] ==> R"
  (fn major::prems =>
isabelle