src/Provers/induct_method.ML
2006-01-19 ago setup: theory -> theory;
2006-01-14 ago sane ERROR handling;
2006-01-10 ago fix_tac: no warning;
2006-01-07 ago RuleCases.make_common/nested;
2006-01-05 ago RuleCases.strict_mutual_rule;
2005-12-23 ago removed obsolete atomize_old;
2005-12-23 ago proper treatment of nested conjunctions, i.e. simultaneous goals and mutual rules;
2005-12-22 ago simplified setup: removed dest_concls, local_impI, conjI;
2005-12-02 ago introduced new map2, fold
2005-11-29 ago moved nth_list to Pure/library.ML;
2005-11-25 ago induct: insert defs in object-logic form;
2005-11-25 ago fix_tac: proper treatment of major premises in goal;
2005-11-23 ago more robust revert_skolem;
2005-11-23 ago (co)induct: taking;
2005-11-22 ago make coinduct actually work;
2005-11-19 ago induct: CONJUNCTS for multiple goals;
2005-11-16 ago induct: support local definitions to be passed through the induction;
2005-11-10 ago induct method: fixes;
2005-10-28 ago accomodate simplified Thm.lift_rule;
2005-10-21 ago Goal.norm_hhf_rule, Goal.init;
2005-06-14 ago export cases_tac, induct_tac;
2005-04-21 ago Adapted to new interface of instantiation and unification / matching functions.
2005-04-13 ago *** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13 ago *** empty log message ***
2005-03-04 ago Removed practically all references to Library.foldr.
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2004-10-11 ago Induction now preserves the name of the induction variable.
2004-06-21 ago Merged in license change from Isabelle2004
2004-02-21 ago Transitive_Closure: added consumes and case_names attributes
2002-09-30 ago fixes !!-bound vars in induction statement automatically
2002-07-26 ago support for split assumptions in cases (hyps vs. prems);
2002-05-31 ago Changed interface of MetaSimplifier.rewrite_term.
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);