diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Sun Nov 26 13:19:52 2017 +0100
+++ b/src/HOL/Algebra/Coset.thy	Sun Nov 26 21:08:32 2017 +0100
@@ -410,7 +410,7 @@
 text\<open>Alternative characterization of normal subgroups\<close>
 lemma (in group) normal_inv_iff:
      "(N \<lhd> G) = 
-      (subgroup N G & (\<forall>x \<in> carrier G. \<forall>h \<in> N. x \<otimes> h \<otimes> (inv x) \<in> N))"
+      (subgroup N G \<and> (\<forall>x \<in> carrier G. \<forall>h \<in> N. x \<otimes> h \<otimes> (inv x) \<in> N))"
       (is "_ = ?rhs")
 proof
   assume N: "N \<lhd> G"
@@ -476,7 +476,7 @@
   assume "\<exists>h\<in>H. y = x \<otimes> h"
     and x: "x \<in> carrier G"
     and sb: "subgroup H G"
-  then obtain h' where h': "h' \<in> H & x \<otimes> h' = y" by blast
+  then obtain h' where h': "h' \<in> H \<and> x \<otimes> h' = y" by blast
   show "\<exists>h\<in>H. x = y \<otimes> h"
   proof
     show "x = y \<otimes> inv h'" using h' x sb
@@ -593,7 +593,7 @@
 
 definition
   r_congruent :: "[('a,'b)monoid_scheme, 'a set] \<Rightarrow> ('a*'a)set"  ("rcong\<index> _")
-  where "rcong\<^bsub>G\<^esub> H = {(x,y). x \<in> carrier G & y \<in> carrier G & inv\<^bsub>G\<^esub> x \<otimes>\<^bsub>G\<^esub> y \<in> H}"
+  where "rcong\<^bsub>G\<^esub> H = {(x,y). x \<in> carrier G \<and> y \<in> carrier G \<and> inv\<^bsub>G\<^esub> x \<otimes>\<^bsub>G\<^esub> y \<in> H}"
 
 
 lemma (in subgroup) equiv_rcong:
@@ -784,7 +784,7 @@
 lemma (in group) inj_on_f:
     "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> inv a) (H #> a)"
 apply (rule inj_onI)
-apply (subgoal_tac "x \<in> carrier G & y \<in> carrier G")
+apply (subgoal_tac "x \<in> carrier G \<and> y \<in> carrier G")
  prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD])
 apply (simp add: subsetD)
 done
@@ -898,7 +898,7 @@
 definition
   kernel :: "('a, 'm) monoid_scheme \<Rightarrow> ('b, 'n) monoid_scheme \<Rightarrow>  ('a \<Rightarrow> 'b) \<Rightarrow> 'a set"
     \<comment>\<open>the kernel of a homomorphism\<close>
-  where "kernel G H h = {x. x \<in> carrier G & h x = \<one>\<^bsub>H\<^esub>}"
+  where "kernel G H h = {x. x \<in> carrier G \<and> h x = \<one>\<^bsub>H\<^esub>}"
 
 lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
 apply (rule subgroup.intro)