Speedup EQF_INTRO

Author: ordinarymath

src/1/Drule.sml

@@ -618,14 +618,19 @@ fun NOT_EQ_SYM th =
  *                                                                           *
  * [TFM 90.05.08]                                                            *
  * --------------------------------------------------------------------------*)
-
 local
-   val Fth = ASSUME F
+   val eq_F = el 4 $ CONJUNCTS $ SPEC_ALL EQ_CLAUSES;
+   val eq_F' = SYM eq_F
+   val t = (dest_neg o fst o dest_eq) (concl eq_F')
+   (*  ∀t. ¬t ⇔ (t ⇔ F) *)
+   val eq_F' = GEN t eq_F'
 in
    fun EQF_INTRO th =
-      IMP_ANTISYM_RULE (NOT_ELIM th)
-                       (DISCH F (CONTR (dest_neg (concl th)) Fth))
-      handle HOL_ERR _ => raise ERR "EQF_INTRO" ""
+     let val t' = dest_neg (concl th)
+     in
+     EQ_MP (SPEC t' eq_F') th
+     end
+     handle HOL_ERR _ => raise ERR "EQF_INTRO" ""
 end
 
 (* --------------------------------------------------------------------------*