src/Tools/induct.ML
4 months ago wenzelm 2019-01-04 isabelle update -u control_cartouches;
4 months ago wenzelm 2019-01-03 isabelle update_inner_syntax_cartouches;
15 months ago wenzelm 2018-02-18 tuned signature;
17 months ago wenzelm 2017-12-06 prefer control symbol antiquotations;
2016-06-22 wenzelm 2016-06-22 tuned signature; tuned;
2016-04-12 wenzelm 2016-04-12 Type_Infer.object_logic controls improvement of type inference result;
2016-04-08 wenzelm 2016-04-08 eliminated unused simproc identifier;
2015-12-16 wenzelm 2015-12-16 rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
2015-12-14 wenzelm 2015-12-14 tuned signature;
2015-12-13 wenzelm 2015-12-13 more general types Proof.method / context_tactic; proper context for Method.insert_tac; tuned;
2015-09-25 wenzelm 2015-09-25 moved remaining display.ML to more_thm.ML;
2015-09-09 wenzelm 2015-09-09 simplified simproc programming interfaces;
2015-08-30 wenzelm 2015-08-30 trim context for persistent storage;
2015-07-26 wenzelm 2015-07-26 updated to infer_instantiate;
2015-07-05 wenzelm 2015-07-05 simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
2015-06-25 wenzelm 2015-06-25 tuned signature;
2015-06-25 wenzelm 2015-06-25 tuned;
2015-06-13 wenzelm 2015-06-13 implicit rule for method "cases";
2015-05-30 wenzelm 2015-05-30 tuned -- more direct Thm.renamed_prop;
2015-04-16 wenzelm 2015-04-16 discontinued pointless warnings: commands are only defined inside a theory context;
2015-04-08 wenzelm 2015-04-08 tuned;
2015-04-08 wenzelm 2015-04-08 tuned signature;
2015-04-08 wenzelm 2015-04-08 proper context for Object_Logic operations;
2015-04-06 wenzelm 2015-04-06 local setup of induction tools, with restricted access to auxiliary consts; proper antiquotations for formerly inaccessible consts;
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
2015-04-06 wenzelm 2015-04-06 tuned;
2015-03-29 wenzelm 2015-03-29 tuned;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 wenzelm 2015-03-04 clarified signature;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-26 wenzelm 2014-11-26 added ML antiquotation @{apply n} or @{apply n(k)};
2014-11-09 wenzelm 2014-11-09 proper context for match_tac etc.;
2014-11-09 wenzelm 2014-11-09 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
2014-11-08 wenzelm 2014-11-08 optional proof context for unify operations, for the sake of proper local options;
2014-11-03 wenzelm 2014-11-03 eliminated unused int_only flag (see also c12484a27367); just proper commands;
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2014-10-29 wenzelm 2014-10-29 modernized setup;
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;