src/HOL/Relation.thy
changeset 5608 a82a038a3e7a
parent 4746 a5dcd7e4a37d
child 5978 fa2c2dd74f8c
     1.1 --- a/src/HOL/Relation.thy	Fri Oct 02 10:44:20 1998 +0200
     1.2 +++ b/src/HOL/Relation.thy	Fri Oct 02 14:28:39 1998 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  Relation = Prod +
     1.6  consts
     1.7 -    id          :: "('a * 'a)set"               (*the identity relation*)
     1.8 +    Id          :: "('a * 'a)set"               (*the identity relation*)
     1.9      O           :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr 60)
    1.10      converse    :: "('a*'b) set => ('b*'a) set"     ("(_^-1)" [1000] 999)
    1.11      "^^"        :: "[('a*'b) set,'a set] => 'b set" (infixl 90)
    1.12 @@ -15,7 +15,7 @@
    1.13      trans       :: "('a * 'a)set => bool"       (*transitivity predicate*)
    1.14      Univalent   :: "('a * 'b)set => bool"
    1.15  defs
    1.16 -    id_def        "id == {p. ? x. p = (x,x)}"
    1.17 +    Id_def        "Id == {p. ? x. p = (x,x)}"
    1.18      comp_def      "r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
    1.19      converse_def   "r^-1 == {(y,x). (x,y):r}"
    1.20      Domain_def    "Domain(r) == {x. ? y. (x,y):r}"