src/HOL/Ord.thy
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