src/HOL/Library/simps_case_conv.ML
6 months ago wenzelm 2019-01-04 isabelle update -u control_cartouches;
6 months ago Andreas Lochbihler 2019-01-01 new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
2016-06-23 wenzelm 2016-06-23 tuned signature;
2016-06-22 wenzelm 2016-06-22 tuned;
2016-06-22 wenzelm 2016-06-22 tuned signature; tuned;
2016-04-13 wenzelm 2016-04-13 eliminated "xname" and variants;
2015-12-09 wenzelm 2015-12-09 tuned;
2015-07-09 noschinl 2015-07-09 case_of_simps: do not split for types with a single constructor
2015-06-02 noschinl 2015-06-02 simps_of_case: Better error if split rule is not an equality
2015-06-02 noschinl 2015-06-02 simps_of_case: allow Drule.dummy_thm as ignored split rule
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
2015-03-08 wenzelm 2015-03-08 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 tuned signature -- prefer qualified names;
2015-03-03 traytel 2015-03-03 eliminated some clones of Proof_Context.cterm_of
2014-11-09 wenzelm 2014-11-09 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
2014-08-21 wenzelm 2014-08-21 tuned signature -- define some elementary operations earlier;
2014-07-23 wenzelm 2014-07-23 tuned message;
2014-03-22 wenzelm 2014-03-22 more antiquotations;
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;
2013-12-31 wenzelm 2013-12-31 proper context for norm_hhf and derived operations; clarified tool context in some boundary cases;
2013-11-12 blanchet 2013-11-12 ported 'Simps_Case_Conv' to use new 'Ctr_Sugar' abstraction
2013-09-06 wenzelm 2013-09-06 more standard header;
2013-09-06 noschinl 2013-09-06 allowed less exhaustive patterns
2013-09-06 noschinl 2013-09-06 added simps_of_case and case_of_simps to convert between simps and case rules