src/HOL/Orderings.thy
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;
2006-11-18 haftmann 2006-11-18 re-eliminated thm trichotomy
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-15 haftmann 2006-11-15 added transitivity rules, reworking of min/max lemmas
2006-11-13 haftmann 2006-11-13 introduces preorders
2006-11-09 wenzelm 2006-11-09 modified less/less_eq syntax to avoid "x < y < z" etc.;
2006-11-08 haftmann 2006-11-08 abstract ordering theories
2006-11-07 haftmann 2006-11-07 made locale partial_order compatible with axclass order; changed import order; consecutive changes
2006-11-07 wenzelm 2006-11-07 renamed 'const_syntax' to 'notation'; proper notation for fixed variables;
2006-11-06 haftmann 2006-11-06 removed dependency of ord on eq
2006-11-05 wenzelm 2006-11-05 fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
2006-10-23 haftmann 2006-10-23 cleanup in ML setup code
2006-10-20 haftmann 2006-10-20 cleaned up
2006-10-16 haftmann 2006-10-16 fixed print translations for bounded quantification
2006-09-26 haftmann 2006-09-26 tuned syntax for <= <
2006-09-19 haftmann 2006-09-19 added operational equality
2006-07-04 ballarin 2006-07-04 Method intro_locales replaced by intro_locales and unfold_locales.
2006-06-20 ballarin 2006-06-20 Restructured locales with predicates: import is now an interpretation. New method intro_locales.
2006-05-16 wenzelm 2006-05-16 tuned concrete syntax -- abbreviation/const_syntax;
2006-05-13 wenzelm 2006-05-13 reactivated translations for less/less_eq;
2006-05-02 wenzelm 2006-05-02 replaced syntax/translations by abbreviation;
2006-05-01 paulson 2006-05-01 some facts about min, max and add, diff
2006-03-17 haftmann 2006-03-17 renamed op < <= to Orderings.less(_eq)
2006-02-14 haftmann 2006-02-14 added theory of executable rational numbers
2006-01-30 haftmann 2006-01-30 adaptions to codegen_package
2006-01-17 haftmann 2006-01-17 substantial improvements in code generator
2005-10-17 wenzelm 2005-10-17 change_claset/simpset;
2005-08-03 avigad 2005-08-03 added extra transitivity rules
2005-07-15 wenzelm 2005-07-15 tuned fold on terms;
2005-07-13 paulson 2005-07-13 generlization of some "nat" theorems
2005-07-07 obua 2005-07-07 1) all theorems in Orderings can now be given as a parameter 2) new function Theory.defs_of 3) new functions Defs.overloading_info and Defs.is_overloaded
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-05-31 wenzelm 2005-05-31 tuned;
2005-05-11 nipkow 2005-05-11 Added thms by Brian Huffmann
2005-04-25 ballarin 2005-04-25 Subsumption of locale interpretations.
2005-04-23 wenzelm 2005-04-23 _gt, _gt: syntax instead of consts;
2005-04-21 nipkow 2005-04-21 tuning locales
2005-04-20 nipkow 2005-04-20 Used locale interpretations everywhere.
2005-03-24 ballarin 2005-03-24 Transitivity reasoner ignores types amenable to linear arithmetic. These are currently nat, int, real. Fixed IsaMakefile.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-02-10 nipkow 2005-02-10 Moved oderings from HOL into the new Orderings.thy