src/Provers/induct_method.ML
2002-05-07 ago use eq_thm_prop instead of slightly inadequate eq_thm;
2002-01-26 ago cases: really append cases_default;
2002-01-17 ago MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
2001-11-28 ago join_rules RuleCases.save;
2001-11-19 ago induct method: localize rews for rule;
2001-11-12 ago induct: rule_versions produces localized variants;
2001-11-12 ago proper handling of mutual rules (esp. for sets);
2001-11-05 ago Method.trace ctxt;
2001-10-31 ago induct: internalize ``missing'' consumes-facts from goal state
2001-10-30 ago induct: cases are extracted from rulified rule;
2001-10-16 ago dest_env: norm_term on rhs;
2001-10-16 ago simplified resolveq_cases_tac for cases, separate version for induct;
2001-10-15 ago Tactic.rewrite_cterm;
2001-10-14 ago moved rulify to ObjectLogic;
2001-10-14 ago use ObjectLogic stuff;
2001-10-12 ago removed vars_of, concls_of;
2001-10-04 ago proof by cases and induction on types and sets (used to be specific for HOL);