Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/Fix.thy
Sun, 07 Feb 2010 10:15:15 -0800 huffman add lemma iterate_below_fix file | diff | annotate
Sat, 16 Jan 2010 17:15:28 +0100 haftmann dropped some old primrecs and some constdefs file | diff | annotate
Tue, 10 Nov 2009 06:30:19 -0800 huffman add lemma parallel_fix_ind file | diff | annotate
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 file | diff | annotate
Tue, 16 Dec 2008 21:31:55 -0800 huffman remove cvs Id tags file | diff | annotate
Sun, 22 Jun 2008 23:02:40 +0200 huffman use new-style abbreviation/notation for fix syntax file | diff | annotate
Thu, 19 Jun 2008 00:02:08 +0200 huffman add lemma iterate_iterate file | diff | annotate
Thu, 12 Jun 2008 22:30:00 +0200 huffman change orientation of fix_eqI and convert to rule_format; file | diff | annotate
Fri, 18 Jan 2008 20:34:28 +0100 huffman add space to binder syntax file | diff | annotate
Fri, 18 Jan 2008 20:22:07 +0100 huffman change lemma admD to rule_format file | diff | annotate
Sun, 21 Oct 2007 14:21:48 +0200 wenzelm modernized specifications ('definition', 'abbreviation', 'notation'); file | diff | annotate
Sun, 06 Nov 2005 00:22:03 +0100 huffman add proof of Bekic's theorem: fix_cprod file | diff | annotate
Sat, 05 Nov 2005 21:52:13 +0100 huffman put iterate and fix in separate sections; added Letrec file | diff | annotate
Sat, 05 Nov 2005 21:50:37 +0100 huffman renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM file | diff | annotate
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 file | diff | annotate
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 file | diff | annotate
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 file | diff | annotate
Mon, 10 Oct 2005 05:30:02 +0200 huffman new syntax translations for continuous lambda abstraction file | diff | annotate
Thu, 22 Sep 2005 19:06:05 +0200 huffman cleaned up file | diff | annotate
Tue, 26 Jul 2005 18:22:55 +0200 huffman add theorem fix_defined_iff; cleaned up file | diff | annotate
Thu, 23 Jun 2005 22:11:55 +0200 huffman added theorems fix_strict, fix_defined, fix_id, fix_const file | diff | annotate
Tue, 14 Jun 2005 04:05:15 +0200 huffman renamed theorem cont2cont_CF1L_rev2 to cont2cont_lambda file | diff | annotate
Fri, 03 Jun 2005 23:33:48 +0200 huffman cleaned up proof of cont_Ifix file | diff | annotate
Thu, 26 May 2005 02:24:08 +0200 huffman added defaultsort declaration file | diff | annotate
Thu, 26 May 2005 00:30:24 +0200 huffman moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun file | diff | annotate
Wed, 25 May 2005 09:44:34 +0200 wenzelm removed LICENCE note -- everything is subject to Isabelle licence as file | diff | annotate
Tue, 24 May 2005 05:03:54 +0200 huffman Moved admissibility definitions and lemmas to a separate theory file | diff | annotate
Wed, 18 May 2005 23:49:52 +0200 huffman shortened proof of adm_disj file | diff | annotate
Wed, 18 May 2005 23:29:36 +0200 huffman cleaned up and shortened some proofs file | diff | annotate
Wed, 27 Apr 2005 00:47:38 +0200 huffman Added binder syntax for fix file | diff | annotate
Thu, 31 Mar 2005 00:10:35 +0200 huffman changed comments to text blocks, cleaned up a few proofs file | diff | annotate
Fri, 04 Mar 2005 23:23:47 +0100 huffman fix headers file | diff | annotate
Fri, 04 Mar 2005 23:12:36 +0100 huffman converted to new-style theories, and combined numbered files file | diff | annotate
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004 file | diff | annotate
Sat, 03 Nov 2001 01:41:26 +0100 wenzelm GPLed; file | diff | annotate
Tue, 09 Jan 2001 15:32:27 +0100 nipkow *** empty log message *** file | diff | annotate
Fri, 24 Jul 1998 13:44:27 +0200 berghofe Adapted to new datatype package. file | diff | annotate
Tue, 10 Mar 1998 18:33:13 +0100 oheimb renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin file | diff | annotate
Fri, 10 Oct 1997 19:02:28 +0200 wenzelm fixed dots; file | diff | annotate
Sun, 25 May 1997 16:59:40 +0200 slotosch Moved the classes flat chfin from Fix to Pcpo. file | diff | annotate
Sun, 25 May 1997 16:17:09 +0200 slotosch Eliminated the prediates flat,chfin file | diff | annotate
Wed, 26 Mar 1997 17:58:48 +0100 nipkow Added "discrete" CPOs and modified IMP to use those rather than "lift" file | diff | annotate
Mon, 17 Feb 1997 10:57:11 +0100 slotosch Changes of HOLCF from Oscar Slotosch: file | diff | annotate
Fri, 29 Nov 1996 12:15:33 +0100 oheimb renamed is_flat to flat, file | diff | annotate
Thu, 12 Sep 1996 17:28:06 +0200 oheimb added comment on is_flat file | diff | annotate
Tue, 25 Jun 1996 13:18:54 +0200 berghofe Changed argument order of nat_rec. file | diff | annotate
Tue, 06 Feb 1996 12:42:31 +0100 clasohm expanded tabs file | diff | annotate
Wed, 20 Dec 1995 16:28:51 +0100 regensbu changed predicate flat to is_flat in theory Fix.thy file | diff | annotate
Thu, 29 Jun 1995 16:28:40 +0200 regensbu The curried version of HOLCF is now just called HOLCF. The old file | diff | annotate
Wed, 21 Jun 1995 15:14:58 +0200 clasohm removed \...\ inside strings file | diff | annotate
Wed, 29 Jun 1994 12:03:41 +0200 clasohm added parentheses made necessary by change of constrain's precedence file | diff | annotate
Wed, 19 Jan 1994 17:35:01 +0100 nipkow Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF file | diff | annotate
less more (0) tip
isabelle