converse: syntax \<inverse>;
authorwenzelm
Mon Oct 30 18:25:10 2000 +0100 (2000-10-30)
changeset 10358ef2a753cda2a
parent 10357 0d0cac129618
child 10359 445e3b87f28b
converse: syntax \<inverse>;
src/HOL/Relation.thy
     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