| Tue, 21 Dec 2010 09:18:29 +0100 |
haftmann |
evaluator separating static and dynamic operations
|
changeset |
files
|
| Tue, 21 Dec 2010 09:18:29 +0100 |
haftmann |
canonical handling of theory context argument
|
changeset |
files
|
| Tue, 21 Dec 2010 09:16:03 +0100 |
haftmann |
merged
|
changeset |
files
|
| Tue, 21 Dec 2010 08:40:39 +0100 |
haftmann |
evaluator separating static and dynamic operations
|
changeset |
files
|
| Tue, 21 Dec 2010 08:40:39 +0100 |
haftmann |
program is separate argument to serializer
|
changeset |
files
|
| Tue, 21 Dec 2010 07:45:04 +0100 |
haftmann |
more explicit structure for serializer invocation
|
changeset |
files
|
| Tue, 21 Dec 2010 08:38:03 +0100 |
nipkow |
merged
|
changeset |
files
|
| Tue, 21 Dec 2010 08:37:48 +0100 |
nipkow |
tuned proof
|
changeset |
files
|
| 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
|
| Mon, 20 Dec 2010 23:36:58 +0100 |
wenzelm |
Cygwin: Poly/ML 5.4.0 requires libgmp3;
|
changeset |
files
|