| Sat, 27 Nov 2010 13:12:10 -0800 |
huffman |
renamed several HOLCF theorems (listed in NEWS)
|
file |
diff |
annotate
|
| Wed, 10 Nov 2010 14:20:47 -0800 |
huffman |
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
|
file |
diff |
annotate
|
| Wed, 27 Oct 2010 13:54:18 -0700 |
huffman |
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
|
file |
diff |
annotate
|
| Tue, 12 Oct 2010 05:48:15 -0700 |
huffman |
reformulate lemma cont2cont_lub and move to Cont.thy
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 12:07:52 +0200 |
wenzelm |
renamed command 'defaultsort' to 'default_sort';
|
file |
diff |
annotate
|
| Tue, 06 Apr 2010 09:27:03 +0200 |
krauss |
tuned proof (no induction needed); removed unused lemma and fuzzy comment
|
file |
diff |
annotate
|
| Tue, 23 Mar 2010 13:42:12 -0700 |
huffman |
minimize dependencies
|
file |
diff |
annotate
|
| Tue, 23 Mar 2010 09:39:21 -0700 |
huffman |
move letrec stuff to new file HOLCF/ex/Letrec.thy
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 23:02:43 -0700 |
huffman |
define CLetrec using Pair, fst, snd instead of cpair, cfst, csnd
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 22:43:21 -0700 |
huffman |
convert lemma fix_cprod to use Pair, fst, snd
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 21:11:54 -0700 |
huffman |
remove admw predicate
|
file |
diff |
annotate
|
| Sun, 14 Mar 2010 19:48:33 -0700 |
huffman |
use headers consistently
|
file |
diff |
annotate
|
| 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
|