src/ZF/ZF.ML
changeset 664 ba39b4984f5a
parent 516 1957113f0d7d
child 688 4dddc8d0c384
--- a/src/ZF/ZF.ML	Mon Oct 31 15:49:58 1994 +0100
+++ b/src/ZF/ZF.ML	Mon Oct 31 16:39:20 1994 +0100
@@ -35,7 +35,6 @@
   val equality_iffI	: thm
   val equals0D		: thm
   val equals0I		: thm
-  val ex1_functional	: thm
   val InterD		: thm
   val InterE		: thm
   val InterI		: thm
@@ -233,12 +232,6 @@
 
 (*** Rules for Replace -- the derived form of replacement ***)
 
-val ex1_functional = prove_goal ZF.thy
-    "[| EX! z. P(a,z);  P(a,b);  P(a,c) |] ==> b = c"
- (fn prems=>
-  [ (cut_facts_tac prems 1),
-    (best_tac FOL_dup_cs 1) ]);
-
 val Replace_iff = prove_goalw ZF.thy [Replace_def]
     "b : {y. x:A, P(x,y)}  <->  (EX x:A. P(x,b) & (ALL y. P(x,y) --> y=b))"
  (fn _=>