author wenzelm Mon Oct 30 18:25:10 2000 +0100 (2000-10-30) changeset 10358 ef2a753cda2a parent 10357 0d0cac129618 child 10359 445e3b87f28b
converse: syntax \<inverse>;
 src/HOL/Relation.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Relation.thy	Mon Oct 30 18:24:42 2000 +0100
1.2 +++ b/src/HOL/Relation.thy	Mon Oct 30 18:25:10 2000 +0100
1.3 @@ -1,4 +1,4 @@
1.4 -(*  Title:      Relation.thy
1.5 +(*  Title:      HOL/Relation.thy
1.6      ID:         \$Id\$
1.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1.8      Copyright   1996  University of Cambridge
1.9 @@ -7,9 +7,12 @@
1.10  Relation = Product_Type +
1.11
1.12  constdefs
1.13 -  converse :: "('a*'b) set => ('b*'a) set"               ("(_^-1)" [1000] 999)
1.14 -    "r^-1 == {(y,x). (x,y):r}"
1.15 +  converse :: "('a * 'b) set => ('b * 'a) set"    ("(_^-1)" [1000] 999)
1.16 +  "r^-1 == {(y, x). (x, y) : r}"
1.17 +syntax (xsymbols)
1.18 +  converse :: "('a * 'b) set => ('b * 'a) set"    ("(_\\<inverse>)" [1000] 999)
1.19
1.20 +constdefs
1.21    comp  :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set"  (infixr "O" 60)
1.22      "r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
1.23
1.24 @@ -48,7 +51,6 @@
1.25
1.26  syntax
1.27    reflexive :: "('a * 'a)set => bool"       (*reflexivity over a type*)
1.28 -
1.29  translations
1.30    "reflexive" == "refl UNIV"
1.31
```