diff -r 638bbd5a4a3b -r 667b5ea637dd src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Relation.thy	Sat Apr 08 22:51:06 2006 +0200
@@ -58,9 +58,9 @@
   inv_image :: "('b * 'b) set => ('a => 'b) => ('a * 'a) set"
   "inv_image r f == {(x, y). (f x, f y) : r}"
 
-abbreviation (output)
+abbreviation
   reflexive :: "('a * 'a) set => bool"  -- {* reflexivity over a type *}
-  "reflexive = refl UNIV"
+  "reflexive == refl UNIV"
 
 
 subsection {* The identity relation *}