| Mon, 20 Dec 2010 22:27:26 +0100 | boehmes | merged | changeset | files |
| Mon, 20 Dec 2010 22:02:57 +0100 | boehmes | avoid ML structure aliases (especially single-letter abbreviations) | changeset | files |
| Mon, 20 Dec 2010 21:04:45 +0100 | boehmes | added an additional beta reduction: unfolding of special quantifiers might leave terms unnormalized wrt to beta reductions | changeset | files |
| Mon, 20 Dec 2010 11:11:51 -0800 | huffman | merged | changeset | files |
| Mon, 20 Dec 2010 10:57:01 -0800 | huffman | configure domain package to work with HOL option type | changeset | files |
| 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 |