src/Tools/induct.ML
2014-08-19 wenzelm 2014-08-19 simplified type Proof.method;
2014-03-31 wenzelm 2014-03-31 some shortcuts for chunks, which sometimes avoid bulky string output;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-20 wenzelm 2014-03-20 enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
2014-03-06 wenzelm 2014-03-06 more uniform check_const/read_const;
2014-03-06 wenzelm 2014-03-06 tuned signature -- more uniform check_type_name/read_type_name; proper reports for read_type_name (lost in 710bc66f432c);
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-08-23 wenzelm 2013-08-23 tuned signature;
2013-07-27 wenzelm 2013-07-27 standardized aliases;
2013-07-17 wenzelm 2013-07-17 take context from static theory, not dynamic theory certificate;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-04-09 wenzelm 2013-04-09 discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems'; print timing as tracing, to keep it out of the way in Proof General; no timing of control commands, especially relevant for Proof General;
2013-03-30 wenzelm 2013-03-30 more item markup; tuned signature;
2013-03-29 wenzelm 2013-03-29 Pretty.item markup for improved readability of lists of items;
2012-10-09 wenzelm 2012-10-09 clarified Local_Defs.add_def(s): refrain from hard-wiring Thm.def_binding_optional; clarified Generic_Target.define: avoid duplicate def binding via Local_Defs.add_def;
2012-09-29 wenzelm 2012-09-29 more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
2012-03-21 wenzelm 2012-03-21 prefer explicitly qualified exception List.Empty;
2012-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2011-11-06 wenzelm 2011-11-06 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute; misc tuning;
2011-11-03 wenzelm 2011-11-03 tuned signature;
2011-10-16 wenzelm 2011-10-16 added Term.dummy_pattern conveniences;
2011-10-12 wenzelm 2011-10-12 tuned signature;
2011-10-12 wenzelm 2011-10-12 misc tuning and clarification;
2011-10-12 wenzelm 2011-10-12 tuned ML style;
2011-09-20 nipkow 2011-09-20 New proof method "induction" that gives induction hypotheses the name IH.
2011-09-16 nipkow 2011-09-16 when applying induction rules, remove names of assumptions that come with the rule in case the rule is transformed by the simplifier due to instantiations
2011-08-17 wenzelm 2011-08-17 modernized signature of Term.absfree/absdummy; eliminated obsolete Term.list_abs_free;
2011-06-09 wenzelm 2011-06-09 renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
2011-06-09 wenzelm 2011-06-09 simplified Name.variant -- discontinued builtin fold_map;
2011-06-08 wenzelm 2011-06-08 more robust exception pattern General.Subscript;
2011-04-27 wenzelm 2011-04-27 reorganized fixes as specialized (global) name space;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2010-12-17 wenzelm 2010-12-17 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
2010-08-25 wenzelm 2010-08-25 renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
2010-06-24 wenzelm 2010-06-24 misc tuning;
2010-06-24 wenzelm 2010-06-24 tuned auxiliary structures;
2010-06-24 wenzelm 2010-06-24 Net.encode_type;
2010-05-17 wenzelm 2010-05-17 prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
2010-04-30 wenzelm 2010-04-30 slightly more standard induct_simp_add/del attributes; provide explicit context for internal addsimps;
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-03-07 wenzelm 2010-03-07 modernized structure Local_Defs;
2010-02-27 wenzelm 2010-02-27 type/const name: explicitly allow abbreviations as well;
2010-02-25 wenzelm 2010-02-25 clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;
2010-01-30 berghofe 2010-01-30 Added infrastructure for simplifying equality constraints in cases rules.
2010-01-10 berghofe 2010-01-10 Added infrastructure for simplifying equality constraints. Option (no_simp) restores old behaviour of induct method.
2009-11-25 haftmann 2009-11-25 normalized uncurry take/drop
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-11-01 wenzelm 2009-11-01 adapted Item_Net; tuned;
2009-11-01 wenzelm 2009-11-01 modernized structure Rule_Cases;
2009-10-29 wenzelm 2009-10-29 separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
2009-10-02 wenzelm 2009-10-02 eliminated dead code;
2009-08-28 wenzelm 2009-08-28 modernized messages -- eliminated ctyp/cterm operations;
2009-07-25 wenzelm 2009-07-25 eliminated redundant Library.multiply;
2009-07-24 wenzelm 2009-07-24 renamed functor InductFun to Induct;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-17 wenzelm 2009-07-17 tuned/modernized Envir operations;
2009-03-26 wenzelm 2009-03-26 simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
2009-03-17 wenzelm 2009-03-17 adapted to general Item_Net;