src/HOL/Orderings.thy
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
2011-09-13 huffman 2011-09-13 tuned proofs
2011-08-08 wenzelm 2011-08-08 misc tuning -- eliminated old-fashioned rep_thm;
2011-08-03 haftmann 2011-08-03 tuned
2011-07-16 haftmann 2011-07-16 consolidated bot and top classes, tuned notation
2011-07-13 haftmann 2011-07-13 uniqueness lemmas for bot and top
2011-07-13 haftmann 2011-07-13 moved lemmas bot_less and less_top to classes bot and top respectively
2011-07-13 haftmann 2011-07-13 tightened specification of classes bot and top: uniqueness of top and bot elements
2011-06-29 wenzelm 2011-06-29 tuned signature;
2011-06-29 wenzelm 2011-06-29 simplified/unified Simplifier.mk_solver;
2011-05-13 wenzelm 2011-05-13 clarified map_simpset versus Simplifier.map_simpset_global;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Mixfix; eliminated slightly odd no_syn convenience;
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2010-12-08 haftmann 2010-12-08 bot comes before top, inf before sup etc.
2010-12-08 haftmann 2010-12-08 nice syntax for lattice INFI, SUPR; various *_apply rules for lattice operations on fun; more default simplification rules
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-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-08-26 haftmann 2010-08-26 formerly unnamed infix impliciation now named HOL.implies
2010-08-25 wenzelm 2010-08-25 renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
2010-08-24 hoelzl 2010-08-24 moved generic lemmas in Probability to HOL
2010-08-23 blanchet 2010-08-23 "no_atp" fact that leads to unsound proofs in Sledgehammer
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
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-04 haftmann 2010-05-04 locale predicates of classes carry a mandatory "class" prefix
2010-03-18 blanchet 2010-03-18 now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
2010-03-04 hoelzl 2010-03-04 Add dense_le, dense_le_bounded, field_le_mult_one_interval.
2010-02-25 wenzelm 2010-02-25 more antiquotations;
2010-02-22 haftmann 2010-02-22 distributed theory Algebras to theories Groups and Lattices
2010-02-11 wenzelm 2010-02-11 modernized translations; formal markup of @{syntax_const} and @{const_syntax}; minor tuning;
2010-02-10 haftmann 2010-02-10 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2010-01-28 haftmann 2010-01-28 new theory Algebras.thy for generic algebraic structures
2010-01-04 haftmann 2010-01-04 moved name duplicates to end of theory; reduced warning noise
2009-12-11 haftmann 2009-12-11 moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-10-09 haftmann 2009-10-09 tuned order of lemmas
2009-10-07 haftmann 2009-10-07 added bot_boolE, top_boolI
2009-07-26 wenzelm 2009-07-26 replaced old METAHYPS by FOCUS; eliminated homegrown SUBGOAL combinator -- beware of exception Subscript in body; modernized functor names; minimal tuning of sources; reactivated dead quasi.ML (ever used?);
2009-07-14 haftmann 2009-07-14 code attributes use common underscore convention
2009-04-15 haftmann 2009-04-15 code generator bootstrap theory src/Tools/Code_Generator.thy
2009-03-30 wenzelm 2009-03-30 simplified 'print_orders' command;
2009-03-26 wenzelm 2009-03-26 simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
2009-03-15 wenzelm 2009-03-15 simplified attribute setup;
2009-03-13 wenzelm 2009-03-13 simplified method setup;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2009-03-06 haftmann 2009-03-06 added strict_mono predicate
2009-02-26 berghofe 2009-02-26 Fixed nonexhaustive match problem in decomp, to make it fail more gracefully in case assumptions are not of the form (Trueprop $ ...).
2009-02-06 haftmann 2009-02-06 session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there