--- a/ROOT.ML Fri Nov 25 13:33:27 1994 +0100
+++ b/ROOT.ML Fri Nov 25 13:34:33 1994 +0100
@@ -22,7 +22,6 @@
use "../Provers/classical.ML";
use "../Provers/simplifier.ML";
use "../Provers/splitter.ML";
-use "../Provers/ind.ML";
(** Applying HypsubstFun to generate hyp_subst_tac **)
@@ -60,9 +59,6 @@
val HOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I]
addSEs [exE,ex1E] addEs [allE];
-structure HOL_Induction = InductionFun(struct val spec=spec end);
-open HOL_Induction;
-
use "simpdata.ML";
use_thy "Ord";
use_thy "subset";
@@ -79,7 +75,7 @@
use "add_ind_def.ML";
use "intr_elim.ML";
use "indrule.ML";
-use "Inductive.ML";
+use_thy "Inductive";
use_thy "Finite";
use_thy "List";