diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Algebra/Coset.thy
--- 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"