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 |