src/ZF/Tools/inductive_package.ML
changeset 28839 32d498cf7595
parent 28678 d93980a6c3cb
child 28965 1de908189869
equal deleted inserted replaced
28838:d5db6dfcb34a 28839:32d498cf7595
   260   val basic_elim_tac =
   260   val basic_elim_tac =
   261       REPEAT (SOMEGOAL (eresolve_tac (Ind_Syntax.elim_rls @ Su.free_SEs)
   261       REPEAT (SOMEGOAL (eresolve_tac (Ind_Syntax.elim_rls @ Su.free_SEs)
   262                 ORELSE' bound_hyp_subst_tac))
   262                 ORELSE' bound_hyp_subst_tac))
   263       THEN prune_params_tac
   263       THEN prune_params_tac
   264           (*Mutual recursion: collapse references to Part(D,h)*)
   264           (*Mutual recursion: collapse references to Part(D,h)*)
   265       THEN fold_tac part_rec_defs;
   265       THEN (PRIMITIVE (fold_rule part_rec_defs));
   266 
   266 
   267   (*Elimination*)
   267   (*Elimination*)
   268   val elim = rule_by_tactic basic_elim_tac
   268   val elim = rule_by_tactic basic_elim_tac
   269                  (unfold RS Ind_Syntax.equals_CollectD)
   269                  (unfold RS Ind_Syntax.equals_CollectD)
   270 
   270