| Mon, 20 Dec 2010 10:48:01 -0800 | huffman | make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction | changeset | files |
| Mon, 20 Dec 2010 09:48:16 -0800 | huffman | simplify proofs | changeset | files |
| Mon, 20 Dec 2010 09:41:55 -0800 | huffman | beta-reduction simproc uses lemma Abs_cfun_inverse2 instead of beta_cfun, to be more robust against eta-contraction | changeset | files |
| Mon, 20 Dec 2010 08:26:47 -0800 | huffman | configure domain package to work with HOL sum type | changeset | files |
| Mon, 20 Dec 2010 07:50:47 -0800 | huffman | replace list_map function with an abbreviation | changeset | files |
| Mon, 20 Dec 2010 18:48:13 +0100 | blanchet | merged | changeset | files |