src/HOL/Tools/inductive.ML
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;
2011-11-27 wenzelm 2011-11-27 just one data slot per module; tuned;
2011-11-27 wenzelm 2011-11-27 tuned;
2011-11-27 wenzelm 2011-11-27 more antiquotations;
2011-11-27 wenzelm 2011-11-27 misc tuning;
2011-11-19 wenzelm 2011-11-19 added ML antiquotation @{attributes};
2011-10-28 wenzelm 2011-10-28 uniform Local_Theory.declaration with explicit params;
2011-10-28 wenzelm 2011-10-28 tuned signature -- refined terminology;
2011-09-10 haftmann 2011-09-10 more modularization
2011-04-27 wenzelm 2011-04-27 more precise position information via Variable.add_fixes_binding;
2011-04-20 wenzelm 2011-04-20 eliminated Display.string_of_thm_without_context; tuned whitespace;
2011-04-17 wenzelm 2011-04-17 added Binding.print convenience, which includes quote already;
2011-04-16 wenzelm 2011-04-16 eliminated old List.nth; tuned;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-16 wenzelm 2011-04-16 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
2011-02-21 blanchet 2011-02-21 renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
2010-12-17 wenzelm 2010-12-17 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
2010-12-08 haftmann 2010-12-08 primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
2010-12-03 bulwahn 2010-12-03 tuned
2010-11-03 wenzelm 2010-11-03 replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
2010-09-09 haftmann 2010-09-09 only conceal primitive definition theorems, not predicate names
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-23 bulwahn 2010-08-23 introducing simplification equations for inductive sets; added data structure for storing equations; rewriting retrieval of simplification equation for inductive predicates and sets
2010-08-12 haftmann 2010-08-12 Named_Target.theory_init
2010-08-11 haftmann 2010-08-11 renamed Theory_Target to the more appropriate Named_Target
2010-08-01 bulwahn 2010-08-01 inductive_simps learns to have more tool compliance
2010-07-26 wenzelm 2010-07-26 inductive_cases: crude parallelization via Par_List.map;
2010-07-21 wenzelm 2010-07-21 make SML/NJ happy, by adhoc type-constraints;
2010-07-07 bulwahn 2010-07-07 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
2010-06-01 blanchet 2010-06-01 removed "nitpick_intro" attribute -- Nitpick noew uses Spec_Rules instead
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-05-17 wenzelm 2010-05-17 tuned;
2010-05-16 wenzelm 2010-05-16 prefer structure Parse_Spec;
2010-05-05 haftmann 2010-05-05 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)