| changeset 21404 | eb85850d3eb7 |
| parent 20318 | 0e0ea63fe768 |
| child 23350 | 50c5b0912a0c |
--- a/src/HOL/Algebra/Coset.thy Fri Nov 17 02:19:55 2006 +0100 +++ b/src/HOL/Algebra/Coset.thy Fri Nov 17 02:20:03 2006 +0100 @@ -30,7 +30,7 @@ assumes coset_eq: "(\<forall>x \<in> carrier G. H #> x = x <# H)" abbreviation - normal_rel :: "['a set, ('a, 'b) monoid_scheme] \<Rightarrow> bool" (infixl "\<lhd>" 60) + normal_rel :: "['a set, ('a, 'b) monoid_scheme] \<Rightarrow> bool" (infixl "\<lhd>" 60) where "H \<lhd> G \<equiv> normal H G"