src/HOL/Ord.thy
2000-11-13 nipkow 2000-11-13 Removed > and >= again.
2000-11-10 nipkow 2000-11-10 new: > and >=
2000-10-17 nipkow 2000-10-17 <= -> \<le>
2000-05-18 wenzelm 2000-05-18 fewer consts declared as global;
1999-08-25 wenzelm 1999-08-25 proper bootstrap of HOL theory and packages;
1999-08-17 wenzelm 1999-08-17 replaced HOL_quantifiers flag by "HOL" print mode; simplified HOL basic syntax (more orthogonal);
1999-06-29 nipkow 1999-06-29 Bad translation fixed.
1999-04-27 wenzelm 1999-04-27 hol_setup, simpdata_setup;
1999-03-18 nipkow 1999-03-18 New bounded quantifier syntax: !x<i. P etc
1998-11-24 wenzelm 1998-11-24 setup Blast.setup; setup Clasimp.setup;
1998-11-16 wenzelm 1998-11-16 Classical.setup, attrib_setup;
1998-02-20 nipkow 1998-02-20 Congruence rules use == in premises now. New class linord.
1997-10-20 wenzelm 1997-10-20 adapted to qualified names;
1997-10-09 wenzelm 1997-10-09 fixed infix syntax;
1997-05-08 nipkow 1997-05-08 Modified def of Least, which, as Markus correctly complained, looked like Minimal. Derived the old def for nat in NatDef as Least_nat_def.
1997-02-14 wenzelm 1997-02-14 fixed comment;
1997-02-12 nipkow 1997-02-12 New class "order" and accompanying changes. In particular reflexivity of <= is now one rewrite rule.
1996-11-27 wenzelm 1996-11-27 fixed comment; added "op <", "op <=" syntax; added symbol syntax;
1996-09-23 paulson 1996-09-23 New infix syntax: breaks line BEFORE operator
1995-11-29 clasohm 1995-11-29 removed quotes from types in consts and syntax sections
1995-03-20 clasohm 1995-03-20 changed syntax of "if"
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application