src/HOL/ex/Refute_Examples.thy
changeset 63901 4ce989e962e0
parent 62148 e410c6287103
child 66453 cc19f7ca2ed6
     1.1 --- a/src/HOL/ex/Refute_Examples.thy	Fri Sep 16 18:09:13 2016 +0200
     1.2 +++ b/src/HOL/ex/Refute_Examples.thy	Fri Sep 16 21:28:09 2016 +0200
     1.3 @@ -128,7 +128,7 @@
     1.4  refute [expect = genuine]
     1.5  oops
     1.6  
     1.7 -lemma "EX! x. P x"
     1.8 +lemma "\<exists>!x. P x"
     1.9  refute [expect = genuine]
    1.10  oops
    1.11  
    1.12 @@ -152,7 +152,7 @@
    1.13  refute [expect = genuine]
    1.14  oops
    1.15  
    1.16 -lemma "(\<exists>x. P x) \<longrightarrow> (EX! x. P x)"
    1.17 +lemma "(\<exists>x. P x) \<longrightarrow> (\<exists>!x. P x)"
    1.18  refute [expect = genuine]
    1.19  oops
    1.20  
    1.21 @@ -220,11 +220,11 @@
    1.22  refute [expect = genuine]
    1.23  oops
    1.24  
    1.25 -lemma "EX! P. P"
    1.26 +lemma "\<exists>!P. P"
    1.27  refute [expect = none]
    1.28  by auto
    1.29  
    1.30 -lemma "EX! P. P x"
    1.31 +lemma "\<exists>!P. P x"
    1.32  refute [expect = genuine]
    1.33  oops
    1.34  
    1.35 @@ -280,7 +280,7 @@
    1.36  
    1.37  text \<open>Axiom of Choice: first an incorrect version ...\<close>
    1.38  
    1.39 -lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (EX!f. \<forall>x. P x (f x))"
    1.40 +lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>!f. \<forall>x. P x (f x))"
    1.41  refute [expect = genuine]
    1.42  oops
    1.43  
    1.44 @@ -290,7 +290,7 @@
    1.45  refute [maxsize = 4, expect = none]
    1.46  by (simp add: choice)
    1.47  
    1.48 -lemma "(\<forall>x. EX!y. P x y) \<longrightarrow> (EX!f. \<forall>x. P x (f x))"
    1.49 +lemma "(\<forall>x. \<exists>!y. P x y) \<longrightarrow> (\<exists>!f. \<forall>x. P x (f x))"
    1.50  refute [maxsize = 2, expect = none]
    1.51  apply auto
    1.52    apply (simp add: ex1_implies_ex choice)