ROOT.ML

 
 structure Hypsubst_Data =
   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 HOL.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
   end;
 
 structure Hypsubst = HypsubstFun(Hypsubst_Data);
 open Hypsubst;
 
-(** Applying ClassicalFun to create a classical prover **)
-structure Classical_Data =
+(*** Applying ClassicalFun to create a classical prover ***)
+structure Classical_Data = 
   struct
-  val sizef = size_of_thm
-  val mp = mp
-  val not_elim = notE
-  val classical = classical
+  val sizef	= size_of_thm
+  val mp	= mp
+  val not_elim	= notE
+  val classical	= classical
   val hyp_subst_tacs=[hyp_subst_tac]
   end;
 
 structure Classical = ClassicalFun(Classical_Data);
 open Classical;

                        addSEs [conjE,disjE,impCE,FalseE,iffE];
 
 (*Quantifier rules*)
 val HOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I]
                      addSEs [exE,ex1E] addEs [allE];
-
-val HOL_dup_cs = prop_cs addSIs [allI] addIs [exCI,ex1I]
-                         addSEs [exE,ex1E] addEs [all_dupE];
 
 structure HOL_Induction = InductionFun(struct val spec=spec end);
 open HOL_Induction;
 
 use     "simpdata.ML";