| Tue, 21 Dec 2010 07:23:21 +0100 | haftmann | HOLogic.mk_id | changeset | files |
| Tue, 21 Dec 2010 06:53:20 +0100 | blanchet | avoid weird symbols in path | changeset | files |
| Tue, 21 Dec 2010 06:06:28 +0100 | blanchet | mechanism to keep SMT input and output files around in Mirabelle | changeset | files |
| Tue, 21 Dec 2010 04:33:17 +0100 | blanchet | proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them; | changeset | files |
| Tue, 21 Dec 2010 03:56:51 +0100 | blanchet | added "smt_triggers" option to experiment with triggers in Sledgehammer; | changeset | files |
| Tue, 21 Dec 2010 01:12:17 +0100 | blanchet | enable E weight generation with unofficial latest version of E (tentatively called E 1.2B) -- backed by Judgment Day | changeset | files |