Wed, 17 Aug 2011 14:32:48 -0700 | huffman | IsaMakefile: target HOLCF-Library now compiles HOL/HOLCF/Library instead of HOL/Library | changeset | files |
Wed, 17 Aug 2011 13:10:49 -0700 | huffman | merged | changeset | files |
Wed, 17 Aug 2011 13:10:11 -0700 | huffman | Lim.thy: generalize and simplify proofs of LIM/LIMSEQ theorems | changeset | files |
Wed, 17 Aug 2011 11:39:09 -0700 | huffman | add lemma tendsto_compose_eventually; use it to shorten some proofs | changeset | files |