src/HOLCF/Porder0.ML
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2001-11-03 wenzelm 2001-11-03 GPLed;
2000-09-15 paulson 2000-09-15 renamed (most of...) the select rules
2000-07-05 paulson 2000-07-05 massive tidy-up: goal -> Goal, remove use of prems, etc.
2000-07-04 paulson 2000-07-04 removed most batch-style proofs
2000-06-28 paulson 2000-06-28 tidying and unbatchifying
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1997-12-16 wenzelm 1997-12-16 expandshort;
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-06-26 nipkow 1997-06-26 Tuned Franz's proofs.
1997-05-25 slotosch 1997-05-25 eliminated the constant less by the introduction of the axclass sq_ord added explicit type ::'a::po in the following theorems: minimal2UU,antisym_less_inverse,box_less,not_less2not_eq,monofun_pair and dist_eqI (in domain-package) added instances instance fun :: (term,sq_ord)sq_ord instance "->" :: (term,sq_ord)sq_ord instance "**" :: (sq_ord,sq_ord)sq_ord instance "*" :: (sq_ord,sq_ord)sq_ord instance "++" :: (pcpo,pcpo)sq_ord instance u :: (sq_ord)sq_ord instance lift :: (term)sq_ord instance discr :: (term)sq_ord
1997-04-24 slotosch 1997-04-24 moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML
1997-03-26 nipkow 1997-03-26 Added "discrete" CPOs and modified IMP to use those rather than "lift"
1997-02-17 slotosch 1997-02-17 New file for theorems of Porder0 Dervie the prperties of partial orders from the axiomatic type class po