src/HOL/Tools/inductive.ML
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-03 wenzelm 2015-04-03 more uniform "verbose" option to print name space;
2015-03-31 wenzelm 2015-03-31 clarified role of naming for background theory: transform_binding (e.g. for "concealed" flag) uses naming of hypothetical context;
2015-03-31 wenzelm 2015-03-31 tuned signature;
2015-03-29 wenzelm 2015-03-29 ind_cases: clarified preparation of arguments;
2015-03-06 wenzelm 2015-03-06 clarified context;
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 tuned signature -- prefer qualified names;
2015-03-03 traytel 2015-03-03 eliminated some clones of Proof_Context.cterm_of
2015-02-11 wenzelm 2015-02-11 proper context; eliminated clone;
2015-02-10 wenzelm 2015-02-10 misc tuning;
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 haftmann 2014-11-26 do not conceal inductive predicate names properly, following 4a3747517552
2014-11-26 haftmann 2014-11-26 tuned
2014-11-12 wenzelm 2014-11-12 prefer independent parallel map where user input is processed -- avoid non-deterministic feedback in error situations;
2014-11-10 wenzelm 2014-11-10 proper context for assume_tac (atac remains as fall-back without context);
2014-11-07 wenzelm 2014-11-07 eliminated pointless check -- command definitions are subject to theory context;
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-21 wenzelm 2014-08-21 tuned signature -- define some elementary operations earlier;
2014-08-19 wenzelm 2014-08-19 tuned signature -- moved type src to Token, without aliases;
2014-03-31 wenzelm 2014-03-31 some shortcuts for chunks, which sometimes avoid bulky string output;
2014-03-22 wenzelm 2014-03-22 avoid hard-wired theory names;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-11 wenzelm 2014-03-11 tuned signature;
2014-03-10 wenzelm 2014-03-10 abstract type Name_Space.table; clarified pretty_locale_deps: sort strings; clarified Proof_Context.update_cases: Name_Space.del_table hides name space entry as well;
2014-03-08 wenzelm 2014-03-08 modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121); proper context for global data; tuned signature;
2014-01-22 wenzelm 2014-01-22 tuned signature;
2013-12-31 wenzelm 2013-12-31 proper context for norm_hhf and derived operations; clarified tool context in some boundary cases;
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-09-30 wenzelm 2013-09-30 tuned signature;
2013-09-30 wenzelm 2013-09-30 eliminated clone of Inductive.mk_cases_tac;
2013-07-27 wenzelm 2013-07-27 standardized aliases;
2013-05-17 wenzelm 2013-05-17 proper option quick_and_dirty;
2013-04-27 wenzelm 2013-04-27 uniform Proof.context for hyp_subst_tac;
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;
2013-03-27 wenzelm 2013-03-27 tuned signature and module arrangement;
2013-01-08 wenzelm 2013-01-08 prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
2012-11-30 wenzelm 2012-11-30 added 'print_inductives' command;
2012-11-30 wenzelm 2012-11-30 print formal entities with markup;
2012-11-26 wenzelm 2012-11-26 tuned command descriptions;
2012-09-12 wenzelm 2012-09-12 removed obsolete argument "int" and thus made SML/NJ happy (cf. 03bee3a6a1b7);
2012-09-05 wenzelm 2012-09-05 discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
2012-05-10 wenzelm 2012-05-10 tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
2012-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-03-15 wenzelm 2012-03-15 prefer formally checked @{keyword} parser;
2012-03-15 wenzelm 2012-03-15 declare minor keywords via theory header;
2012-03-14 wenzelm 2012-03-14 more parallel inductive_cases; more explicit indication of def names;
2012-03-12 wenzelm 2012-03-12 some grouping of Par_List operations, to adjust granularity;
2012-02-27 wenzelm 2012-02-27 prefer cut_tac, where it is clear that the special variants cut_rules_tac or cut_facts_tac are not required;
2012-01-14 wenzelm 2012-01-14 discontinued old-style Term.list_abs in favour of plain Term.abs;
2012-01-14 wenzelm 2012-01-14 renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
2012-01-14 wenzelm 2012-01-14 discontinued old-style Term.list_all_free in favour of plain Logic.all;
2011-12-02 wenzelm 2011-12-02 more antiquotations;
2011-11-27 wenzelm 2011-11-27 permissive update for improved "tool compliance"; tuned;