| 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
|
| Mon, 11 Oct 2010 21:35:31 -0700 |
huffman |
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
|
file |
diff |
annotate
|
| Thu, 07 Oct 2010 13:33:06 -0700 |
huffman |
add lemma typedef_ideal_completion
|
file |
diff |
annotate
|
| Wed, 06 Oct 2010 10:49:27 -0700 |
huffman |
major reorganization/simplification of HOLCF type classes:
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 12:07:52 +0200 |
wenzelm |
renamed command 'defaultsort' to 'default_sort';
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 21:28:09 +0200 |
wenzelm |
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 12:52:51 -0700 |
huffman |
remove LaTeX hyperref warnings by avoiding antiquotations within section headings
|
file |
diff |
annotate
|
| Sun, 14 Mar 2010 19:48:33 -0700 |
huffman |
use headers consistently
|
file |
diff |
annotate
|
| Wed, 10 Mar 2010 15:20:13 -0800 |
huffman |
adapt HOLCF to use Nat_Bijection library
|
file |
diff |
annotate
|
| Sun, 10 Jan 2010 18:43:45 +0100 |
berghofe |
Adapted to changes in induct method.
|
file |
diff |
annotate
|
| Thu, 22 Oct 2009 15:50:12 +0200 |
wenzelm |
renamed f_inv_onto_f to f_inv_into_f (cf. 764547b68538);
|
file |
diff |
annotate
|
| Sun, 18 Oct 2009 22:19:05 +0200 |
wenzelm |
fixed proof (cf. d1d4d7a08a66);
|
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
|
| Thu, 26 Mar 2009 20:08:55 +0100 |
wenzelm |
interpretation/interpret: prefixes are mandatory by default;
|
file |
diff |
annotate
|
| Mon, 16 Mar 2009 15:10:59 -0700 |
huffman |
clean up proofs
|
file |
diff |
annotate
|
| Fri, 13 Mar 2009 07:30:47 -0700 |
huffman |
introduce new helper functions; clean up proofs
|
file |
diff |
annotate
|
| Tue, 30 Dec 2008 11:10:01 +0100 |
ballarin |
Merged.
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 21:10:53 +0100 |
ballarin |
More porting to new locales.
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 21:31:55 -0800 |
huffman |
remove cvs Id tags
|
file |
diff |
annotate
|
| Tue, 25 Nov 2008 23:26:44 +0100 |
huffman |
renamed lemma compact_minimal to compact_bot_minimal
|
file |
diff |
annotate
|
| Tue, 01 Jul 2008 01:28:07 +0200 |
huffman |
universal bifinite domain
|
file |
diff |
annotate
|