src/HOL/ZF/HOLZF.thy
changeset 63901 4ce989e962e0
parent 63167 0909deb8059b
child 67443 3abf6a722518
     1.1 --- a/src/HOL/ZF/HOLZF.thy	Fri Sep 16 18:09:13 2016 +0200
     1.2 +++ b/src/HOL/ZF/HOLZF.thy	Fri Sep 16 21:28:09 2016 +0200
     1.3 @@ -270,7 +270,7 @@
     1.4    by (auto simp add: Fun_def Sep Domain)
     1.5  
     1.6  
     1.7 -lemma unique_fun_value: "\<lbrakk>isFun f; Elem x (Domain f)\<rbrakk> \<Longrightarrow> ?! y. Elem (Opair x y) f"
     1.8 +lemma unique_fun_value: "\<lbrakk>isFun f; Elem x (Domain f)\<rbrakk> \<Longrightarrow> \<exists>!y. Elem (Opair x y) f"
     1.9    by (auto simp add: Domain isFun_def)
    1.10  
    1.11  lemma fun_value_in_range: "\<lbrakk>isFun f; Elem x (Domain f)\<rbrakk> \<Longrightarrow> Elem (f\<acute>x) (Range f)"