| Wed, 20 Jul 2011 00:37:42 +0200 | blanchet | avoid calling "Term.is_first_order" (indirectly) on a term with loose de Bruijns -- this is not necessary anyway because of the Abs check in "simple_translate_lambdas" | changeset | files |
| Wed, 20 Jul 2011 00:37:42 +0200 | blanchet | remove offset from Mirabelle output | changeset | files |
| Tue, 19 Jul 2011 11:15:38 +0200 | krauss | the HOL4PROOFS setting is actually HOL4_PROOFS | changeset | files |