src/HOLCF/Cfun.thy
Tue, 02 Mar 2010 17:21:10 -0800 huffman proper names for types cfun, sprod, ssum
Tue, 02 Mar 2010 23:59:54 +0100 wenzelm proper (type_)notation;
Wed, 17 Feb 2010 08:19:46 -0800 huffman fix warnings about duplicate simp rules
Thu, 11 Feb 2010 23:00:22 +0100 wenzelm modernized translations;
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
Wed, 06 May 2009 00:57:29 -0700 huffman replace cont2cont_apply with cont_apply; add new cont2cont lemmas
Wed, 14 Jan 2009 18:18:48 -0800 huffman minimize dependencies
Wed, 14 Jan 2009 17:11:29 -0800 huffman change to simpler, more extensible continuity simproc
Tue, 16 Dec 2008 21:31:55 -0800 huffman remove cvs Id tags
Thu, 11 Dec 2008 16:50:18 +0100 wenzelm pcpodef package: state two goals, instead of encoded conjunction;
Wed, 10 Dec 2008 17:15:26 -0800 huffman cleaned up some proofs in Cfun.thy
Tue, 01 Jul 2008 02:19:53 +0200 huffman replace lub (range Y) with (LUB i. Y i)
Thu, 19 Jun 2008 20:34:28 +0200 huffman add lemma cfcomp_LAM
Thu, 31 Jan 2008 21:23:14 +0100 huffman instances for class discrete_cpo
Fri, 18 Jan 2008 20:34:28 +0100 huffman add space to binder syntax
Thu, 17 Jan 2008 00:51:20 +0100 huffman change class axiom chfin to rule_format
Wed, 16 Jan 2008 22:41:49 +0100 huffman change class axiom ax_flat to rule_format
Mon, 14 Jan 2008 18:25:20 +0100 huffman added lemmas lub_distribs
Thu, 10 Jan 2008 17:06:41 +0100 huffman declare ch2ch_LAM [simp]
Fri, 04 Jan 2008 00:01:02 +0100 huffman new instance proofs for classes finite_po, chfin, flat
Wed, 02 Jan 2008 18:57:40 +0100 huffman move lemmas from Cont.thy to Ffun.thy;
Thu, 20 Dec 2007 03:06:20 +0100 huffman move bottom-related stuff back into Pcpo.thy
Tue, 18 Dec 2007 22:18:31 +0100 huffman add class ppo of pointed partial orders;
Sun, 21 Oct 2007 16:27:42 +0200 wenzelm modernized specifications ('definition', 'axiomatization');
Sun, 21 Oct 2007 14:21:48 +0200 wenzelm modernized specifications ('definition', 'abbreviation', 'notation');
Thu, 31 May 2007 14:01:58 +0200 wenzelm moved HOLCF tools to canonical place;
Wed, 24 May 2006 01:47:25 +0200 huffman add theorem cfcomp_strict
Sat, 05 Nov 2005 21:50:37 +0100 huffman renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
Sat, 05 Nov 2005 21:42:24 +0100 huffman add line breaks to Rep_CFun syntax
Fri, 04 Nov 2005 23:15:11 +0100 huffman moved adm_chfindom from Fix.thy to Cfun.thy
Fri, 04 Nov 2005 22:26:09 +0100 huffman add print translation: Abs_CFun f => LAM x. f x
Thu, 03 Nov 2005 01:28:22 +0100 huffman add translation for wildcard pattern
Thu, 03 Nov 2005 01:11:39 +0100 huffman change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
Thu, 03 Nov 2005 00:57:35 +0100 huffman cleaned up; ch2ch_Rep_CFun is a simp rule
Tue, 11 Oct 2005 23:22:12 +0200 huffman rearranged subsections; added theorems expand_cfun_eq, expand_cfun_less
Mon, 10 Oct 2005 05:46:17 +0200 huffman add names to infix declarations
Mon, 10 Oct 2005 05:30:02 +0200 huffman new syntax translations for continuous lambda abstraction
Mon, 10 Oct 2005 04:38:26 +0200 huffman removed Istrictify; simplified some proofs
Tue, 26 Jul 2005 18:27:16 +0200 huffman cleaned up
Wed, 06 Jul 2005 00:07:34 +0200 huffman use new pcpodef package
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Tue, 14 Jun 2005 03:50:20 +0200 huffman moved continuity simproc to a separate file
Wed, 08 Jun 2005 00:04:38 +0200 huffman added theorem injection_less
Fri, 03 Jun 2005 23:23:55 +0200 huffman removed dependencies on MF2 lemmas; removed some obsolete theorems; cleaned up many proofs; renamed less_cfun2 to less_cfun_ext
Fri, 27 May 2005 01:28:51 +0200 huffman use TypedefPcpo for all class instances
Fri, 27 May 2005 00:24:02 +0200 huffman Use TypedefPcpo theorem for po instance
Fri, 27 May 2005 00:16:18 +0200 huffman use thelub_const lemma
Thu, 26 May 2005 04:41:56 +0200 huffman rewrote continuous isomorphism section, cleaned up
Wed, 25 May 2005 09:44:34 +0200 wenzelm removed LICENCE note -- everything is subject to Isabelle licence as
Mon, 23 May 2005 23:32:07 +0200 huffman moved continuity simproc to Cfun.thy
Thu, 31 Mar 2005 03:03:22 +0200 huffman added theorems eta_cfun and cont2cont_eta
Thu, 10 Mar 2005 20:22:45 +0100 huffman fixed filename in header
Tue, 08 Mar 2005 00:11:49 +0100 huffman reordered and arranged for document generation, cleaned up some proofs
Fri, 04 Mar 2005 23:23:47 +0100 huffman fix headers
Fri, 04 Mar 2005 23:12:36 +0100 huffman converted to new-style theories, and combined numbered files
less more (0) tip