src/HOL/UNITY/ELT.thy

--- a/src/HOL/UNITY/ELT.thy	Wed Dec 08 13:52:36 1999 +0100
+++ b/src/HOL/UNITY/ELT.thy	Wed Dec 08 13:53:29 1999 +0100
@@ -32,9 +32,6 @@
   givenBy :: "['a => 'b] => 'a set set"
     "givenBy f == range (%B. f-`` B)"
 
-  funPair      :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c"
-    "funPair f g == %x. (f x, g x)"
-
   (*visible version of the LEADS-TO relation*)
   leadsETo :: "['a set, 'a set set, 'a set] => 'a program set"
                                         ("(3_/ leadsTo[_]/ _)" [80,0,80] 80)