--- a/src/HOL/Algebra/Coset.thy Sun Apr 09 18:51:11 2006 +0200
+++ b/src/HOL/Algebra/Coset.thy Sun Apr 09 18:51:13 2006 +0200
@@ -27,12 +27,9 @@
locale normal = subgroup + group +
assumes coset_eq: "(\<forall>x \<in> carrier G. H #> x = x <# H)"
-
-syntax
- "@normal" :: "['a set, ('a, 'b) monoid_scheme] \<Rightarrow> bool" (infixl "\<lhd>" 60)
-
-translations
- "H \<lhd> G" == "normal H G"
+abbreviation
+ normal_rel :: "['a set, ('a, 'b) monoid_scheme] \<Rightarrow> bool" (infixl "\<lhd>" 60)
+ "H \<lhd> G \<equiv> normal H G"
subsection {*Basic Properties of Cosets*}