src/HOLCF/Discrete.thy
Mon, 22 Mar 2010 12:52:51 -0700 huffman remove LaTeX hyperref warnings by avoiding antiquotations within section headings
Fri, 08 May 2009 16:19:51 -0700 huffman rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
Tue, 16 Dec 2008 21:31:55 -0800 huffman remove cvs Id tags
Thu, 31 Jan 2008 21:23:14 +0100 huffman instances for class discrete_cpo
Thu, 17 Jan 2008 00:51:20 +0100 huffman change class axiom chfin to rule_format
Mon, 14 Jan 2008 20:28:59 +0100 huffman class bifinite supersedes class dcpo; remove unnecessary dcpo stuff
Mon, 14 Jan 2008 19:25:21 +0100 huffman new-style class instantiation
Fri, 04 Jan 2008 00:01:02 +0100 huffman new instance proofs for classes finite_po, chfin, flat
Wed, 02 Jan 2008 18:27:07 +0100 huffman added dcpo instance proofs
Sun, 21 Oct 2007 14:21:48 +0200 wenzelm modernized specifications ('definition', 'abbreviation', 'notation');
Sun, 19 Feb 2006 02:11:27 +0100 huffman use minimal imports
Fri, 03 Jun 2005 23:30:31 +0200 huffman replaced cont with cont_def
Wed, 25 May 2005 09:44:34 +0200 wenzelm removed LICENCE note -- everything is subject to Isabelle licence as
Thu, 31 Mar 2005 02:52:49 +0200 huffman cleaned up some proofs
Tue, 08 Mar 2005 00:15:01 +0100 huffman added subsection headings, cleaned up some proofs
Fri, 04 Mar 2005 23:25:06 +0100 huffman add header
Wed, 02 Mar 2005 00:54:06 +0100 huffman converted to new-style theory
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Sat, 01 Dec 2001 18:52:32 +0100 wenzelm renamed class "term" to "type" (actually "HOL.type");
Sat, 03 Nov 2001 01:41:26 +0100 wenzelm GPLed;
Wed, 26 Mar 1997 17:58:48 +0100 nipkow Added "discrete" CPOs and modified IMP to use those rather than "lift"
less more (0) tip