src/HOL/Relation.thy
changeset 21210 c17fd2df4e9e
parent 20716 a6686a8e1b68
child 21404 eb85850d3eb7
     1.1 --- a/src/HOL/Relation.thy	Tue Nov 07 11:47:56 2006 +0100
     1.2 +++ b/src/HOL/Relation.thy	Tue Nov 07 11:47:57 2006 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4    converse :: "('a * 'b) set => ('b * 'a) set"    ("(_^-1)" [1000] 999)
     1.5    "r^-1 == {(y, x). (x, y) : r}"
     1.6  
     1.7 -const_syntax (xsymbols)
     1.8 +notation (xsymbols)
     1.9    converse  ("(_\<inverse>)" [1000] 999)
    1.10  
    1.11  definition