Mon, 06 Dec 2010 11:22:42 -0800 | huffman | remove lemma cont_cfun; | changeset | files |
Mon, 06 Dec 2010 10:08:33 -0800 | huffman | rename lub_fun -> is_lub_fun, thelub_fun -> lub_fun | changeset | files |
Mon, 06 Dec 2010 08:59:58 -0800 | huffman | pcpodef no longer generates _defined lemmas, use _bottom_iff lemmas instead | changeset | files |
Mon, 06 Dec 2010 08:43:52 -0800 | huffman | cpodef no longer generates lemma is_lub_foo, since it is redundant with lub_foo | changeset | files |
Mon, 06 Dec 2010 08:30:00 -0800 | huffman | add lemmas lub_APP, lub_LAM | changeset | files |
Mon, 06 Dec 2010 19:54:56 +0100 | hoelzl | folding on arbitrary Lebesgue integrable functions | changeset | files |