src/HOLCF/Discrete.thy
2010-03-22 huffman 2010-03-22 remove LaTeX hyperref warnings by avoiding antiquotations within section headings
2009-05-08 huffman 2009-05-08 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
2008-12-16 huffman 2008-12-16 remove cvs Id tags
2008-01-31 huffman 2008-01-31 instances for class discrete_cpo
2008-01-17 huffman 2008-01-17 change class axiom chfin to rule_format
2008-01-14 huffman 2008-01-14 class bifinite supersedes class dcpo; remove unnecessary dcpo stuff
2008-01-14 huffman 2008-01-14 new-style class instantiation
2008-01-04 huffman 2008-01-04 new instance proofs for classes finite_po, chfin, flat
2008-01-02 huffman 2008-01-02 added dcpo instance proofs
2007-10-21 wenzelm 2007-10-21 modernized specifications ('definition', 'abbreviation', 'notation');
2006-02-19 huffman 2006-02-19 use minimal imports
2005-06-03 huffman 2005-06-03 replaced cont with cont_def
2005-05-25 wenzelm 2005-05-25 removed LICENCE note -- everything is subject to Isabelle licence as stated in COPYRIGHT file;
2005-03-31 huffman 2005-03-31 cleaned up some proofs
2005-03-08 huffman 2005-03-08 added subsection headings, cleaned up some proofs
2005-03-04 huffman 2005-03-04 add header
2005-03-02 huffman 2005-03-02 converted to new-style theory
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2001-12-01 wenzelm 2001-12-01 renamed class "term" to "type" (actually "HOL.type");
2001-11-03 wenzelm 2001-11-03 GPLed;
1997-03-26 nipkow 1997-03-26 Added "discrete" CPOs and modified IMP to use those rather than "lift"