src/FOLP/simpdata.ML
changeset 1009 eb7c50688405
parent 0 a5a9c433f639
child 1459 d12da312eff4
equal deleted inserted replaced
1008:fa11e1e28bd3 1009:eb7c50688405
   100   val subst_thms	= [subst];
   100   val subst_thms	= [subst];
   101   val dest_red		= dest_red
   101   val dest_red		= dest_red
   102   end;
   102   end;
   103 
   103 
   104 structure FOLP_Simp = SimpFun(FOLP_SimpData);
   104 structure FOLP_Simp = SimpFun(FOLP_SimpData);
   105 structure Induction = InductionFun(struct val spec=IFOLP.spec end);
       
   106 
   105 
   107 (*not a component of SIMP_DATA, but an argument of SIMP_TAC *)
   106 (*not a component of SIMP_DATA, but an argument of SIMP_TAC *)
   108 val FOLP_congs = 
   107 val FOLP_congs = 
   109    [all_cong,ex_cong,eq_cong,
   108    [all_cong,ex_cong,eq_cong,
   110     conj_cong,disj_cong,imp_cong,iff_cong,not_cong] @ pred_congs;
   109     conj_cong,disj_cong,imp_cong,iff_cong,not_cong] @ pred_congs;
   111 
   110 
   112 val IFOLP_rews =
   111 val IFOLP_rews =
   113    [refl_iff_T] @ conj_rews @ disj_rews @ not_rews @ 
   112    [refl_iff_T] @ conj_rews @ disj_rews @ not_rews @ 
   114     imp_rews @ iff_rews @ quant_rews;
   113     imp_rews @ iff_rews @ quant_rews;
   115 
   114 
   116 open FOLP_Simp Induction;
   115 open FOLP_Simp;
   117 
   116 
   118 val auto_ss = empty_ss setauto ares_tac [TrueI];
   117 val auto_ss = empty_ss setauto ares_tac [TrueI];
   119 
   118 
   120 val IFOLP_ss = auto_ss addcongs FOLP_congs addrews IFOLP_rews;
   119 val IFOLP_ss = auto_ss addcongs FOLP_congs addrews IFOLP_rews;
   121 
   120