src/HOLCF/Discrete.thy
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"