src/HOL/Relation.thy
changeset 19363 667b5ea637dd
parent 19323 ec5cd5b1804c
child 19656 09be06943252
     1.1 --- a/src/HOL/Relation.thy	Sat Apr 08 22:12:02 2006 +0200
     1.2 +++ b/src/HOL/Relation.thy	Sat Apr 08 22:51:06 2006 +0200
     1.3 @@ -58,9 +58,9 @@
     1.4    inv_image :: "('b * 'b) set => ('a => 'b) => ('a * 'a) set"
     1.5    "inv_image r f == {(x, y). (f x, f y) : r}"
     1.6  
     1.7 -abbreviation (output)
     1.8 +abbreviation
     1.9    reflexive :: "('a * 'a) set => bool"  -- {* reflexivity over a type *}
    1.10 -  "reflexive = refl UNIV"
    1.11 +  "reflexive == refl UNIV"
    1.12  
    1.13  
    1.14  subsection {* The identity relation *}