src/Provers/induct_method.ML
2007-07-28 wenzelm 2007-07-28 tuned;
2007-07-05 wenzelm 2007-07-05 simplified ObjectLogic.atomize;
2007-07-03 wenzelm 2007-07-03 CONVERSION tactical; Simplifier.rewrite_goal_tac;
2007-05-10 wenzelm 2007-05-10 moved conversions to structure Conv;
2007-04-30 wenzelm 2007-04-30 explicit treatment of legacy_features;
2006-12-18 haftmann 2006-12-18 switched argument order in *.syntax lifters
2006-12-07 wenzelm 2006-12-07 reorganized structure Tactic vs. MetaSimplifier;
2006-12-07 wenzelm 2006-12-07 reorganized structure Goal vs. Tactic;
2006-10-07 wenzelm 2006-10-07 improved LocalDefs.add_def;
2006-09-11 wenzelm 2006-09-11 induct method: renamed 'fixing' to 'arbitrary';
2006-08-02 wenzelm 2006-08-02 simplified Assumption/ProofContext.export;
2006-06-17 wenzelm 2006-06-17 RuleCases.mutual_rule: ctxt; ProofContext.exports: simultaneous facts;
2006-06-12 wenzelm 2006-06-12 tuned Seq/Envir/Unify interfaces;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-02-22 wenzelm 2006-02-22 simplified Pure conjunction;
2006-02-10 wenzelm 2006-02-10 Args/Attrib syntax: Context.generic;
2006-02-06 wenzelm 2006-02-06 Logic.rlist_abs;
2006-01-28 wenzelm 2006-01-28 LocalDefs.add_def;
2006-01-27 wenzelm 2006-01-27 moved theorem tags from Drule to PureThy;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2006-01-14 wenzelm 2006-01-14 sane ERROR handling;
2006-01-10 wenzelm 2006-01-10 fix_tac: no warning;
2006-01-07 wenzelm 2006-01-07 RuleCases.make_common/nested;
2006-01-05 wenzelm 2006-01-05 RuleCases.strict_mutual_rule; export internalize;
2005-12-23 wenzelm 2005-12-23 removed obsolete atomize_old; induct: align_left insts of mutual rules;
2005-12-23 wenzelm 2005-12-23 proper treatment of nested conjunctions, i.e. simultaneous goals and mutual rules;
2005-12-22 wenzelm 2005-12-22 simplified setup: removed dest_concls, local_impI, conjI; improved handling of simultaneous goals: split cases; simplified treatment of mutual rules, which are now specified as a list instead of object-level conjunction (cf. set/type/rule); moved join_rules to RuleCases.mutual_rule;
2005-12-02 haftmann 2005-12-02 introduced new map2, fold
2005-11-29 wenzelm 2005-11-29 moved nth_list to Pure/library.ML;
2005-11-25 wenzelm 2005-11-25 induct: insert defs in object-logic form; export guess_instance;
2005-11-25 wenzelm 2005-11-25 fix_tac: proper treatment of major premises in goal; export atomize/rulify interface; tuned;
2005-11-23 wenzelm 2005-11-23 more robust revert_skolem; tuned;
2005-11-23 wenzelm 2005-11-23 (co)induct: taking; induct set: proper treatment of defs;
2005-11-22 wenzelm 2005-11-22 make coinduct actually work; moved some generic code to Pure/Isar/rule_cases.ML; tuned;
2005-11-19 wenzelm 2005-11-19 induct: CONJUNCTS for multiple goals; added coinduct method; tuned;
2005-11-16 wenzelm 2005-11-16 induct: support local definitions to be passed through the induction; deprecate open rule cases; misc cleanup;
2005-11-10 wenzelm 2005-11-10 induct method: fixes; tuned;
2005-10-28 wenzelm 2005-10-28 accomodate simplified Thm.lift_rule;
2005-10-21 wenzelm 2005-10-21 Goal.norm_hhf_rule, Goal.init;
2005-06-14 wenzelm 2005-06-14 export cases_tac, induct_tac;
2005-04-21 berghofe 2005-04-21 Adapted to new interface of instantiation and unification / matching functions.
2005-04-13 wenzelm 2005-04-13 *** MESSAGE REFERS TO PREVIOUS VERSION *** Scan.peek; Args.local_tyname, Args.local_const;
2005-04-13 wenzelm 2005-04-13 *** empty log message ***
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-10-11 nipkow 2004-10-11 Induction now preserves the name of the induction variable.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-02-21 nipkow 2004-02-21 Transitive_Closure: added consumes and case_names attributes Isar: fixed parameter name handling in simulatneous induction which I had not done properly 2 years ago.
2002-09-30 nipkow 2002-09-30 fixes !!-bound vars in induction statement automatically
2002-07-26 wenzelm 2002-07-26 support for split assumptions in cases (hyps vs. prems);
2002-05-31 berghofe 2002-05-31 Changed interface of MetaSimplifier.rewrite_term.
2002-05-07 wenzelm 2002-05-07 use eq_thm_prop instead of slightly inadequate eq_thm;
2002-01-26 wenzelm 2002-01-26 cases: really append cases_default; cases/induct method: DETERM;
2002-01-17 wenzelm 2002-01-17 MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm; RuleCases.make interface based on term instead of thm;
2001-11-28 wenzelm 2001-11-28 join_rules RuleCases.save;
2001-11-19 wenzelm 2001-11-19 induct method: localize rews for rule;
2001-11-12 wenzelm 2001-11-12 induct: rule_versions produces localized variants;
2001-11-12 wenzelm 2001-11-12 proper handling of mutual rules (esp. for sets);
2001-11-05 wenzelm 2001-11-05 Method.trace ctxt;