src/HOL/Orderings.thy
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
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations;
2007-10-06 wenzelm 2007-10-06 simplified interfaces for outer syntax;
2007-09-29 haftmann 2007-09-29 proper syntax during class specification
2007-09-27 ballarin 2007-09-27 Fixed setup of transitivity reasoner (function decomp).
2007-09-25 ballarin 2007-09-25 Transitivity reasoner gets additional argument of premises to improve integration with simplifier.
2007-09-18 ballarin 2007-09-18 Transitivity reasoner set up for locales order and linorder.
2007-08-24 haftmann 2007-08-24 moved class dense_linear_order to Orderings.thy
2007-08-15 paulson 2007-08-15 ATP blacklisting is now in theory data, attribute noatp
2007-07-24 haftmann 2007-07-24 using class target
2007-07-20 haftmann 2007-07-20 moved class ord from Orderings.thy to HOL.thy
2007-06-19 wenzelm 2007-06-19 tuned;
2007-06-05 haftmann 2007-06-05 tuned boostrap
2007-06-05 haftmann 2007-06-05 merged Code_Generator.thy into HOL.thy
2007-06-03 nipkow 2007-06-03 tuned list comprehension, added lemma
2007-06-01 haftmann 2007-06-01 dropped superfluous name bindings
2007-05-24 haftmann 2007-05-24 rudimentary class target implementation
2007-05-19 nipkow 2007-05-19 unfold min/max in Stefans code generator
2007-05-19 haftmann 2007-05-19 no special treatment in naming of locale predicates stemming form classes
2007-05-17 haftmann 2007-05-17 canonical prefixing of class constants
2007-05-10 haftmann 2007-05-10 tuned
2007-05-09 haftmann 2007-05-09 moved recfun_codegen.ML to Code_Generator.thy
2007-05-06 haftmann 2007-05-06 dropped preorders, unified syntax
2007-04-20 haftmann 2007-04-20 shifted min/max to class order
2007-03-29 haftmann 2007-03-29 dropped legacy ML bindings
2007-03-20 haftmann 2007-03-20 explizit "type" superclass
2007-03-09 haftmann 2007-03-09 *** empty log message ***
2007-03-02 haftmann 2007-03-02 prefix of class interpretation not mandatory any longer
2007-02-28 wenzelm 2007-02-28 tuned ML setup;
2007-02-23 haftmann 2007-02-23 adjusted code lemmas
2007-02-21 krauss 2007-02-21 Fixed print translations for quantifiers a la "ALL x>=t. P x". These used to fail when the other term in the comparison was itself a bound variable, as in "EX y. ALL x>=y. P x".
2007-02-14 haftmann 2007-02-14 added class "preorder"
2007-02-10 haftmann 2007-02-10 changed name of interpretation linorder to order
2007-01-30 haftmann 2007-01-30 changed name of interpretation linorder to order
2007-01-16 haftmann 2007-01-16 renamed locale partial_order to order
2006-12-13 haftmann 2006-12-13 dropped superfluous header
2006-12-10 wenzelm 2006-12-10 hide const linorder.less_eq_less.max linorder.less_eq_less.min;
2006-12-06 wenzelm 2006-12-06 added basic ML bindings;
2006-12-05 wenzelm 2006-12-05 restored notation for less/less_eq (observe proper order of mixfix annotations!); simplified notation for greater/greater_eq, which is only used for input; removed duplicate abbreviations (implicit inheritance);
2006-12-01 haftmann 2006-12-01 some syntax cleanup
2006-11-27 haftmann 2006-11-27 removed HOL structure
2006-11-26 wenzelm 2006-11-26 updated (binder) syntax/notation;