src/HOL/Orderings.thy
2016-03-05 wenzelm 2016-03-05 old HOL syntax is for input only;
2015-12-28 wenzelm 2015-12-28 former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
2015-12-10 paulson 2015-12-10 not_leE -> not_le_imp_less and other tidying
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-12-01 paulson 2015-12-01 Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
2015-11-18 paulson 2015-11-18 New theorems mostly from Peter Gammie
2015-11-11 Andreas Lochbihler 2015-11-11 add various lemmas
2015-11-09 wenzelm 2015-11-09 qualifier is mandatory by default;
2015-10-09 wenzelm 2015-10-09 discontinued specific HTML syntax;
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-04-16 wenzelm 2015-04-16 discontinued pointless warnings: commands are only defined inside a theory context;
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2014-11-13 hoelzl 2014-11-13 import general theorems from AFP/Markov_Models
2014-11-03 wenzelm 2014-11-03 eliminated unused int_only flag (see also c12484a27367); just proper commands;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-06-30 hoelzl 2014-06-30 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
2014-04-12 haftmann 2014-04-12 more operations and lemmas
2014-04-10 wenzelm 2014-04-10 modernized simproc_setup;
2014-04-10 wenzelm 2014-04-10 misc tuning;
2014-03-10 hoelzl 2014-03-10 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
2013-12-27 haftmann 2013-12-27 prefer target-style syntaxx for sublocale
2013-12-25 haftmann 2013-12-25 postponed min/max lemmas until abstract lattice is available
2013-12-25 haftmann 2013-12-25 tuned structure of min/max lemmas
2013-12-24 haftmann 2013-12-24 tuning and augmentation of min/max lemmas; more lemmas and simp rules for abstract lattices with order; tuned proofs
2013-10-18 blanchet 2013-10-18 killed most "no_atp", to make Sledgehammer more complete
2013-08-27 hoelzl 2013-08-27 renamed inner_dense_linorder to dense_linorder
2013-08-27 hoelzl 2013-08-27 renamed typeclass dense_linorder to unbounded_dense_linorder
2013-07-25 haftmann 2013-07-25 factored syntactic type classes for bot and top (by Alessandro Coglio)
2013-05-25 wenzelm 2013-05-25 syntax translations always depend on context;
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-29 wenzelm 2013-03-29 tuned message;
2013-03-26 haftmann 2013-03-26 more uniform style for interpretation and sublocale declarations
2013-03-23 haftmann 2013-03-23 locales for abstract orders
2013-02-20 hoelzl 2013-02-20 split dense into inner_dense_order and no_top/no_bot
2013-02-24 haftmann 2013-02-24 turned example into library for comparing growth of functions
2012-10-10 haftmann 2012-10-10 more explicit code equations
2012-09-29 wenzelm 2012-09-29 more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-04-12 wenzelm 2012-04-12 more standard method setup;
2012-03-17 wenzelm 2012-03-17 'definition' no longer exports the foundational "raw_def";
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 declare command keywords via theory header, including strict checking outside Pure;
2012-03-12 noschinl 2012-03-12 tuned proofs
2012-03-12 noschinl 2012-03-12 tuned simpset
2012-02-26 haftmann 2012-02-26 tuned syntax declarations; tuned structure
2012-02-26 haftmann 2012-02-26 marked candidates for rule declarations
2012-02-23 haftmann 2012-02-23 moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
2012-02-21 haftmann 2012-02-21 reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems
2012-02-19 haftmann 2012-02-19 distributed lattice properties of predicates to places of instantiation
2011-12-19 noschinl 2011-12-19 weaken preconditions on lemmas
2011-12-15 noschinl 2011-12-15 add complementary lemmas for {min,max}_least
2011-10-24 huffman 2011-10-24 instance bool :: linorder
2011-10-24 bulwahn 2011-10-24 removing poor man's dictionary construction which were only for the ancient code generator with no support of type classes
2011-10-21 bulwahn 2011-10-21 replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
2011-10-20 blanchet 2011-10-20 mark "xt..." rules as "no_atp", since they are easy consequences of other better named properties