# HG changeset patch
# User lcp
# Date 783617960 -3600
# Node ID ba39b4984f5a1340ea9ad111f6e8a683e9db75e6
# Parent  dc3f0582e839ceaec0625e0f5960381a5e939e88
ZF/ZF/ex1_functional: moved to FOL/ROOT

diff -r dc3f0582e839 -r ba39b4984f5a src/ZF/ZF.ML
--- 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 _=>