src/HOL/Algebra/UnivPoly.thy
changeset 63901 4ce989e962e0
parent 63167 0909deb8059b
child 64913 3a9eb793fa10
     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Fri Sep 16 18:09:13 2016 +0200
     1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Fri Sep 16 21:28:09 2016 +0200
     1.3 @@ -1429,7 +1429,7 @@
     1.4  
     1.5  theorem UP_universal_property:
     1.6    assumes S: "s \<in> carrier S"
     1.7 -  shows "EX! Phi. Phi \<in> ring_hom P S \<inter> extensional (carrier P) &
     1.8 +  shows "\<exists>!Phi. Phi \<in> ring_hom P S \<inter> extensional (carrier P) &
     1.9      Phi (monom P \<one> 1) = s &
    1.10      (ALL r : carrier R. Phi (monom P r 0) = h r)"
    1.11    using S eval_monom1