--- 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 _=>