src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy
changeset 63901 4ce989e962e0
parent 63882 018998c00003
child 66453 cc19f7ca2ed6
     1.1 --- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Fri Sep 16 18:09:13 2016 +0200
     1.2 +++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Fri Sep 16 21:28:09 2016 +0200
     1.3 @@ -270,7 +270,7 @@
     1.4    quickcheck[expect = counterexample]
     1.5  oops
     1.6  
     1.7 -lemma "(\<exists>x. P x) \<longrightarrow> (EX! x. P x)"
     1.8 +lemma "(\<exists>x. P x) \<longrightarrow> (\<exists>!x. P x)"
     1.9    quickcheck[random, expect = counterexample]
    1.10    quickcheck[expect = counterexample]
    1.11  oops