src/HOLCF/Adm.thy
Fri, 20 Jun 2008 17:43:16 +0200 huffman tweak lemmas adm_all and adm_ball
Thu, 12 Jun 2008 22:14:07 +0200 huffman remove unnecessary import of Ffun;
Wed, 07 May 2008 10:59:51 +0200 berghofe Adm now imports Ffun rather than Cont, because SetPcpo, which imports Adm,
Fri, 18 Jan 2008 20:22:07 +0100 huffman change lemma admD to rule_format
Thu, 17 Jan 2008 21:56:33 +0100 huffman convert lemma lub_mono to rule_format
Thu, 17 Jan 2008 21:44:19 +0100 huffman rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less
Thu, 17 Jan 2008 00:51:20 +0100 huffman change class axiom chfin to rule_format
Mon, 14 Jan 2008 03:49:53 +0100 huffman converted adm_all and adm_ball to rule_format; cleaned up
Thu, 10 Jan 2008 05:36:03 +0100 huffman Compactness subsection with some new lemmas
Thu, 03 Jan 2008 17:22:24 +0100 huffman remove legacy ML bindings
Thu, 03 Jan 2008 16:29:37 +0100 huffman new lemma adm_upward
Wed, 02 Jan 2008 18:57:40 +0100 huffman move lemmas from Cont.thy to Ffun.thy;
Sun, 21 Oct 2007 14:21:48 +0200 wenzelm modernized specifications ('definition', 'abbreviation', 'notation');
Thu, 13 Apr 2006 23:15:44 +0200 huffman add lemma less_UU_iff as default simp rule
Mon, 10 Oct 2005 04:12:31 +0200 huffman added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
Thu, 22 Sep 2005 19:06:34 +0200 huffman added theorem adm_ball
Thu, 07 Jul 2005 18:20:08 +0200 huffman use theorems ch2ch_cont, cont2contlubE
Fri, 01 Jul 2005 01:48:37 +0200 huffman cleaned up; added adm_less to adm_lemmas; added subsection headings
Sat, 25 Jun 2005 01:09:14 +0200 huffman cleaned up
Fri, 03 Jun 2005 23:15:16 +0200 huffman changed to work with new contlubE rule
Thu, 26 May 2005 00:30:24 +0200 huffman moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
Wed, 25 May 2005 09:44:34 +0200 wenzelm removed LICENCE note -- everything is subject to Isabelle licence as
Tue, 24 May 2005 10:55:11 +0200 paulson cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
Tue, 24 May 2005 05:03:54 +0200 huffman Moved admissibility definitions and lemmas to a separate theory
less more (0) tip