src/HOL/UNITY/Extend.thy
changeset 8948 b797cfa3548d
parent 8703 816d8f6513be
child 10064 1a77667b21ef
     1.1 --- a/src/HOL/UNITY/Extend.thy	Wed May 24 18:19:04 2000 +0200
     1.2 +++ b/src/HOL/UNITY/Extend.thy	Wed May 24 18:40:01 2000 +0200
     1.3 @@ -12,6 +12,10 @@
     1.4  
     1.5  constdefs
     1.6  
     1.7 +  (*MOVE to Relation.thy?*)
     1.8 +  Restrict :: "[ 'a set, ('a*'b) set] => ('a*'b) set"
     1.9 +    "Restrict A r == r Int (A <*> UNIV)"
    1.10 +
    1.11    good_map :: "['a*'b => 'c] => bool"
    1.12      "good_map h == surj h & (ALL x y. fst (inv h (h (x,y))) = x)"
    1.13       (*Using the locale constant "f", this is  f (h (x,y))) = x*)