src/ZF/QPair.thy

--- a/src/ZF/QPair.thy	Tue Aug 27 11:07:54 2002 +0200
+++ b/src/ZF/QPair.thy	Tue Aug 27 11:09:33 2002 +0200
@@ -93,13 +93,6 @@
 by (simp add: QSigma_def)
 
 
-(*The general elimination rule*)
-lemma QSigmaE:
-    "[| c: QSigma(A,B);   
-        !!x y.[| x:A;  y:B(x);  c=<x;y> |] ==> P  
-     |] ==> P"
-by (simp add: QSigma_def, blast) 
-
 (** Elimination rules for <a;b>:A*B -- introducing no eigenvariables **)
 
 lemma QSigmaE [elim!]: