src/HOL/Orderings.thy
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
2009-01-21 haftmann 2009-01-21 dropped ID
2008-11-17 haftmann 2008-11-17 tuned unfold_locales invocation
2008-10-24 haftmann 2008-10-24 new classes "top" and "bot"
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-10-07 haftmann 2008-10-07 tuned min/max code generation
2008-08-11 haftmann 2008-08-11 moved class wellorder to theory Orderings
2008-07-29 haftmann 2008-07-29 declare
2008-07-25 haftmann 2008-07-25 added class preorder
2008-06-20 haftmann 2008-06-20 streamlined definitions
2008-06-10 haftmann 2008-06-10 localized Least in Orderings.thy
2008-05-07 berghofe 2008-05-07 - Now imports Code_Setup, rather than Set and Fun, since the theorems about orderings are already needed in Set - Moved "Dense orders" section to Set, since it requires set notation. - The "Order on sets" section is no longer necessary, since it is subsumed by the order on functions and booleans. - Moved proofs of Least_mono and Least_equality to Set, since they require set notation. - In proof of "instance fun :: (type, order) order", use ext instead of expand_fun_eq, since the latter is not yet available. - predicate1I is no longer declared as introduction rule, since it interferes with subsetI
2008-03-29 wenzelm 2008-03-29 purely functional setup of claset/simpset/clasimpset;
2008-03-19 haftmann 2008-03-19 whitespace tuning
2008-03-17 wenzelm 2008-03-17 removed duplicate lemmas;
2008-01-30 haftmann 2008-01-30 dual orders and dual lattices
2007-12-13 haftmann 2007-12-13 clarified heading
2007-11-30 haftmann 2007-11-30 adjustions to due to instance target
2007-11-29 haftmann 2007-11-29 instance command as rudimentary class target
2007-11-10 wenzelm 2007-11-10 Orderings.min/max: no need to qualify consts; removed legacy ML bindings;
2007-10-26 haftmann 2007-10-26 dropped square syntax
2007-10-25 haftmann 2007-10-25 various localizations
2007-10-19 haftmann 2007-10-19 tuned
2007-10-18 haftmann 2007-10-18 localized mono predicate
2007-10-16 haftmann 2007-10-16 global class syntax