src/HOL/Algebra/Coset.thy
changeset 19380 b808efaa5828
parent 16417 9bc16273c2d4
child 19931 fb32b43e7f80
     1.1 --- a/src/HOL/Algebra/Coset.thy	Sun Apr 09 18:51:11 2006 +0200
     1.2 +++ b/src/HOL/Algebra/Coset.thy	Sun Apr 09 18:51:13 2006 +0200
     1.3 @@ -27,12 +27,9 @@
     1.4  locale normal = subgroup + group +
     1.5    assumes coset_eq: "(\<forall>x \<in> carrier G. H #> x = x <# H)"
     1.6  
     1.7 -
     1.8 -syntax
     1.9 -  "@normal" :: "['a set, ('a, 'b) monoid_scheme] \<Rightarrow> bool"  (infixl "\<lhd>" 60)
    1.10 -
    1.11 -translations
    1.12 -  "H \<lhd> G" == "normal H G"
    1.13 +abbreviation
    1.14 +  normal_rel :: "['a set, ('a, 'b) monoid_scheme] \<Rightarrow> bool"  (infixl "\<lhd>" 60)
    1.15 +  "H \<lhd> G \<equiv> normal H G"
    1.16  
    1.17  
    1.18  subsection {*Basic Properties of Cosets*}