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