src/HOL/Relation.thy
changeset 8268 722074b93cdd
parent 7912 0e42be14f136
child 8703 816d8f6513be
     1.1 --- a/src/HOL/Relation.thy	Mon Feb 21 11:16:19 2000 +0100
     1.2 +++ b/src/HOL/Relation.thy	Mon Feb 21 13:57:07 2000 +0100
     1.3 @@ -40,8 +40,8 @@
     1.4    trans  :: "('a * 'a)set => bool"          (*transitivity predicate*)
     1.5      "trans(r) == (!x y z. (x,y):r --> (y,z):r --> (x,z):r)"
     1.6  
     1.7 -  Univalent :: "('a * 'b)set => bool"
     1.8 -    "Univalent r == !x y. (x,y):r --> (!z. (x,z):r --> y=z)"
     1.9 +  univalent :: "('a * 'b)set => bool"
    1.10 +    "univalent r == !x y. (x,y):r --> (!z. (x,z):r --> y=z)"
    1.11  
    1.12    fun_rel_comp :: "['a => 'b, ('b * 'c) set] => ('a => 'c) set"
    1.13      "fun_rel_comp f R == {g. !x. (f x, g x) : R}"