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/Quickcheck_Examples/Quickcheck_Examples.thy
changeset 63901 4ce989e962e0
parent 63882 018998c00003
child 66453 cc19f7ca2ed6 
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Fri Sep 16 18:09:13 2016 +0200
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Fri Sep 16 21:28:09 2016 +0200
@@ -270,7 +270,7 @@
   quickcheck[expect = counterexample]
 oops
 
-lemma "(\<exists>x. P x) \<longrightarrow> (EX! x. P x)"
+lemma "(\<exists>x. P x) \<longrightarrow> (\<exists>!x. P x)"
   quickcheck[random, expect = counterexample]
   quickcheck[expect = counterexample]
 oops
isabelle