# HG changeset patch
# User lcp
# Date 783619750 -3600
# Node ID 4d9f6d83c2bf411971dd388686e798b860e2474a
# Parent  97e9ad6c1c4a57a56622189986292f5c4b541425
FOL/ROOT/FOL_dup_cs: removed as obsolete
FOL/ROOT: no longer proves rev_cut_eq for hyp_subst_tac

diff -r 97e9ad6c1c4a -r 4d9f6d83c2bf src/FOL/ROOT.ML
--- a/src/FOL/ROOT.ML	Mon Oct 31 16:45:19 1994 +0100
+++ b/src/FOL/ROOT.ML	Mon Oct 31 17:09:10 1994 +0100
@@ -28,13 +28,7 @@
   struct
   (*Take apart an equality judgement; otherwise raise Match!*)
   fun dest_eq (Const("Trueprop",_) $ (Const("op =",_)  $ t $ u)) = (t,u);
-
   val imp_intr = impI
-
-  (*etac rev_cut_eq moves an equality to be the last premise. *)
-  val rev_cut_eq = prove_goal IFOL.thy "[| a=b;  a=b ==> R |] ==> R"
-   (fn prems => [ REPEAT(resolve_tac prems 1) ]);
-
   val rev_mp = rev_mp
   val subst = subst
   val sym = sym
@@ -48,10 +42,10 @@
 (*** Applying ClassicalFun to create a classical prover ***)
 structure Classical_Data = 
   struct
-  val sizef = size_of_thm
-  val mp = mp
-  val not_elim = notE
-  val swap = swap
+  val sizef	= size_of_thm
+  val mp	= mp
+  val not_elim	= notE
+  val classical	= classical
   val hyp_subst_tacs=[hyp_subst_tac]
   end;
 
@@ -68,8 +62,9 @@
 val FOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I] 
                      addSEs [exE,ex1E] addEs [allE];
 
-val FOL_dup_cs = prop_cs addSIs [allI] addIs [exCI,ex1I] 
-                         addSEs [exE,ex1E] addEs [all_dupE];
+val ex1_functional = prove_goal FOL.thy
+    "!!a b c. [| EX! z. P(a,z);  P(a,b);  P(a,c) |] ==> b = c"
+ (fn _ => [ (deepen_tac FOL_cs 1 1) ]);
 
 use "simpdata.ML";