src/HOLCF/Fix.thy
Thu, 19 Jun 2008 00:02:08 +0200 huffman add lemma iterate_iterate
Thu, 12 Jun 2008 22:30:00 +0200 huffman change orientation of fix_eqI and convert to rule_format;
Fri, 18 Jan 2008 20:34:28 +0100 huffman add space to binder syntax
Fri, 18 Jan 2008 20:22:07 +0100 huffman change lemma admD to rule_format
Sun, 21 Oct 2007 14:21:48 +0200 wenzelm modernized specifications ('definition', 'abbreviation', 'notation');
Sun, 06 Nov 2005 00:22:03 +0100 huffman add proof of Bekic's theorem: fix_cprod
Sat, 05 Nov 2005 21:52:13 +0100 huffman put iterate and fix in separate sections; added Letrec
Sat, 05 Nov 2005 21:50:37 +0100 huffman renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
Fri, 04 Nov 2005 23:15:45 +0100 huffman moved adm_chfindom from Fix.thy to Cfun.thy; moved admw-related stuff to its own section
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:43:11 +0100 huffman reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
Mon, 10 Oct 2005 05:30:02 +0200 huffman new syntax translations for continuous lambda abstraction
Thu, 22 Sep 2005 19:06:05 +0200 huffman cleaned up
Tue, 26 Jul 2005 18:22:55 +0200 huffman add theorem fix_defined_iff; cleaned up
Thu, 23 Jun 2005 22:11:55 +0200 huffman added theorems fix_strict, fix_defined, fix_id, fix_const
Tue, 14 Jun 2005 04:05:15 +0200 huffman renamed theorem cont2cont_CF1L_rev2 to cont2cont_lambda
Fri, 03 Jun 2005 23:33:48 +0200 huffman cleaned up proof of cont_Ifix
Thu, 26 May 2005 02:24:08 +0200 huffman added defaultsort declaration
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 05:03:54 +0200 huffman Moved admissibility definitions and lemmas to a separate theory
Wed, 18 May 2005 23:49:52 +0200 huffman shortened proof of adm_disj
Wed, 18 May 2005 23:29:36 +0200 huffman cleaned up and shortened some proofs
Wed, 27 Apr 2005 00:47:38 +0200 huffman Added binder syntax for fix
Thu, 31 Mar 2005 00:10:35 +0200 huffman changed comments to text blocks, cleaned up a few 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
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Sat, 03 Nov 2001 01:41:26 +0100 wenzelm GPLed;
Tue, 09 Jan 2001 15:32:27 +0100 nipkow *** empty log message ***
Fri, 24 Jul 1998 13:44:27 +0200 berghofe Adapted to new datatype package.
Tue, 10 Mar 1998 18:33:13 +0100 oheimb renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
Fri, 10 Oct 1997 19:02:28 +0200 wenzelm fixed dots;
Sun, 25 May 1997 16:59:40 +0200 slotosch Moved the classes flat chfin from Fix to Pcpo.
Sun, 25 May 1997 16:17:09 +0200 slotosch Eliminated the prediates flat,chfin
Wed, 26 Mar 1997 17:58:48 +0100 nipkow Added "discrete" CPOs and modified IMP to use those rather than "lift"
Mon, 17 Feb 1997 10:57:11 +0100 slotosch Changes of HOLCF from Oscar Slotosch:
Fri, 29 Nov 1996 12:15:33 +0100 oheimb renamed is_flat to flat,
Thu, 12 Sep 1996 17:28:06 +0200 oheimb added comment on is_flat
Tue, 25 Jun 1996 13:18:54 +0200 berghofe Changed argument order of nat_rec.
Tue, 06 Feb 1996 12:42:31 +0100 clasohm expanded tabs
Wed, 20 Dec 1995 16:28:51 +0100 regensbu changed predicate flat to is_flat in theory Fix.thy
Thu, 29 Jun 1995 16:28:40 +0200 regensbu The curried version of HOLCF is now just called HOLCF. The old
Wed, 21 Jun 1995 15:14:58 +0200 clasohm removed \...\ inside strings
Wed, 29 Jun 1994 12:03:41 +0200 clasohm added parentheses made necessary by change of constrain's precedence
Wed, 19 Jan 1994 17:35:01 +0100 nipkow Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
less more (0) tip