src/HOL/UNITY/Comp.thy
changeset 8128 3a5864b465e2
parent 8122 b43ad07660b9
child 11190 44e157622cb2
     1.1 --- a/src/HOL/UNITY/Comp.thy	Thu Jan 13 17:36:58 2000 +0100
     1.2 +++ b/src/HOL/UNITY/Comp.thy	Fri Jan 14 12:17:53 2000 +0100
     1.3 @@ -26,8 +26,4 @@
     1.4    funPair      :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c"
     1.5      "funPair f g == %x. (f x, g x)"
     1.6  
     1.7 -  (*the set of all sets determined by f alone*)
     1.8 -  givenBy :: "['a => 'b] => 'a set set"
     1.9 -    "givenBy f == range (%B. f-`` B)"
    1.10 -
    1.11  end