src/HOL/Algebra/abstract/Ideal.thy

--- a/src/HOL/Algebra/abstract/Ideal.thy	Sat Feb 10 08:49:36 2001 +0100
+++ b/src/HOL/Algebra/abstract/Ideal.thy	Sat Feb 10 08:52:41 2001 +0100
@@ -13,7 +13,7 @@
 
 defs
   is_ideal_def	"is_ideal I == (ALL a: I. ALL b: I. a + b : I) &
-                               (ALL a: I. - a : I) & <0> : I &
+                               (ALL a: I. - a : I) & 0 : I &
                                (ALL a: I. ALL r. a * r : I)"
   ideal_of_def	"ideal_of S == Inter {I. is_ideal I & S <= I}"
   is_pideal_def	"is_pideal I == (EX a. I = ideal_of {a})"