No longer builds the induction structure (from ../Provers/ind.ML)
authorlcp
Thu, 06 Apr 1995 11:14:51 +0200
changeset 1009 eb7c50688405
parent 1008 fa11e1e28bd3
child 1010 a7693f30065d
No longer builds the induction structure (from ../Provers/ind.ML)
src/FOLP/simpdata.ML
--- a/src/FOLP/simpdata.ML	Thu Apr 06 11:12:35 1995 +0200
+++ b/src/FOLP/simpdata.ML	Thu Apr 06 11:14:51 1995 +0200
@@ -102,7 +102,6 @@
   end;
 
 structure FOLP_Simp = SimpFun(FOLP_SimpData);
-structure Induction = InductionFun(struct val spec=IFOLP.spec end);
 
 (*not a component of SIMP_DATA, but an argument of SIMP_TAC *)
 val FOLP_congs = 
@@ -113,7 +112,7 @@
    [refl_iff_T] @ conj_rews @ disj_rews @ not_rews @ 
     imp_rews @ iff_rews @ quant_rews;
 
-open FOLP_Simp Induction;
+open FOLP_Simp;
 
 val auto_ss = empty_ss setauto ares_tac [TrueI];