src/HOL/Relation.thy
changeset 10786 04ee73606993
parent 10358 ef2a753cda2a
child 10797 028d22926a41
     1.1 --- a/src/HOL/Relation.thy	Fri Jan 05 10:18:46 2001 +0100
     1.2 +++ b/src/HOL/Relation.thy	Fri Jan 05 10:19:14 2001 +0100
     1.3 @@ -31,6 +31,9 @@
     1.4    Range  :: "('a*'b) set => 'b set"
     1.5      "Range(r) == Domain(r^-1)"
     1.6  
     1.7 +  Field :: "('a*'a)set=>'a set"
     1.8 +    "Field r == Domain r Un Range r"
     1.9 +
    1.10    refl   :: "['a set, ('a*'a) set] => bool" (*reflexivity over a set*)
    1.11      "refl A r == r <= A <*> A & (ALL x: A. (x,x) : r)"
    1.12