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