src/HOL/Tools/Function/lexicographic_order.ML
2015-07-25 wenzelm 2015-07-25 updated to infer_instantiate; tuned;
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-07-07 blanchet 2015-07-07 have the installed termination prover take a 'quiet' flag
2015-06-01 wenzelm 2015-06-01 clarified context;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-06 wenzelm 2015-03-06 clarified context;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2014-12-19 wenzelm 2014-12-19 just one data slot per program unit; tuned signature;
2014-10-29 wenzelm 2014-10-29 modernized setup; tuned whitespace;
2014-08-16 wenzelm 2014-08-16 updated to named_theorems; modernized module name and setup;
2014-03-20 wenzelm 2014-03-20 enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
2013-05-13 wenzelm 2013-05-13 retain goal display options when printing error messages, to avoid breakdown for huge goals;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2012-10-15 wenzelm 2012-10-15 tuned message -- avoid extra blank lines;
2012-10-13 wenzelm 2012-10-13 some attempts to unify/simplify pretty_goal;
2012-04-12 wenzelm 2012-04-12 more standard method setup;
2011-12-02 wenzelm 2011-12-02 more antiquotations;
2011-05-13 wenzelm 2011-05-13 clarified map_simpset versus Simplifier.map_simpset_global;
2011-05-13 wenzelm 2011-05-13 proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;
2011-05-12 wenzelm 2011-05-12 prefer plain simpset operations;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-01-13 wenzelm 2011-01-13 more precise pretty printing -- to accomodate Scala message layout;
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-10-05 krauss 2010-10-05 tuned
2010-10-05 krauss 2010-10-05 force less agressively
2010-10-05 krauss 2010-10-05 lexicographic_order: replace parallel map with laziness to avoid wasting cycles on proofs that are not needed
2010-09-03 wenzelm 2010-09-03 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
2010-04-28 krauss 2010-04-28 default termination prover as plain tactic
2010-02-27 wenzelm 2010-02-27 clarified @{const_name} vs. @{const_abbrev};
2010-02-10 haftmann 2010-02-10 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
2010-01-28 haftmann 2010-01-28 new theory Algebras.thy for generic algebraic structures
2010-01-02 krauss 2010-01-02 new year's resolution: reindented code in function package
2009-11-23 krauss 2009-11-23 eliminated dead code and some unused bindings, reported by polyml
2009-11-02 krauss 2009-11-02 lexicographic order: run local descent proofs in parallel
2009-10-30 krauss 2009-10-30 less verbose termination tactics
2009-10-23 krauss 2009-10-23 function package: more standard names for structures and files
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2009-09-18 haftmann 2009-09-18 tuned const_name antiquotations
2009-07-25 wenzelm 2009-07-25 renamed structure Display_Goal to Goal_Display;
2009-07-24 wenzelm 2009-07-24 Display_Goal.pretty_goals: always Markup.subgoal, clarified options;
2009-07-23 wenzelm 2009-07-23 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-07-23 wenzelm 2009-07-23 clarified pretty_goals, pretty_thm_aux: plain context; explicit pretty_goals_without_context, print_goals_without_context; tuned;
2009-07-20 wenzelm 2009-07-20 moved pretty_goals etc. to Display_Goal (required by tracing tacticals); load display.ML after assumption.ML, to accomodate proper contextual theorem display;
2009-07-02 wenzelm 2009-07-02 renamed NamedThmsFun to Named_Thms; simplified/unified names of instances of Named_Thms;
2009-06-23 haftmann 2009-06-23 uniformly capitialized names for subdirectories