diff -r 4939494ed791 -r ce654b0e6d69 src/HOL/Algebra/RingHom.thy --- a/src/HOL/Algebra/RingHom.thy Tue Feb 13 14:24:50 2018 +0100 +++ b/src/HOL/Algebra/RingHom.thy Thu Feb 15 12:11:00 2018 +0100 @@ -39,8 +39,8 @@ assumes "ring R" "ring S" assumes (* morphism: "h \ carrier R \ carrier S" *) hom_closed: "!!x. x \ carrier R ==> h x \ carrier S" - and compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \ y) = h x \\<^bsub>S\<^esub> h y" - and compatible_add: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \ y) = h x \\<^bsub>S\<^esub> h y" + and compatible_mult: "\x y. [| x \ carrier R; y \ carrier R |] ==> h (x \ y) = h x \\<^bsub>S\<^esub> h y" + and compatible_add: "\x y. [| x \ carrier R; y \ carrier R |] ==> h (x \ y) = h x \\<^bsub>S\<^esub> h y" and compatible_one: "h \ = \\<^bsub>S\<^esub>" shows "ring_hom_ring R S h" proof - @@ -72,7 +72,7 @@ lemma ring_hom_ringI3: fixes R (structure) and S (structure) assumes "abelian_group_hom R S h" "ring R" "ring S" - assumes compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \ y) = h x \\<^bsub>S\<^esub> h y" + assumes compatible_mult: "\x y. [| x \ carrier R; y \ carrier R |] ==> h (x \ y) = h x \\<^bsub>S\<^esub> h y" and compatible_one: "h \ = \\<^bsub>S\<^esub>" shows "ring_hom_ring R S h" proof -