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