| Tue, 21 Dec 2010 12:02:05 +0100 |
boehmes |
merged
|
changeset |
files
|
| Tue, 21 Dec 2010 11:05:30 +0100 |
boehmes |
also provide a view on arguments for "external" built-in symbols (similar to "internal" (real) built-in symbols)
|
changeset |
files
|
| Tue, 21 Dec 2010 01:12:14 +0100 |
traytel |
Enabled non fully polymorphic map functions in subtyping
|
changeset |
files
|
| Tue, 21 Dec 2010 11:54:35 +0100 |
wenzelm |
make SML/NJ and Poly/ML agree on the type of "before";
|
changeset |
files
|
| Tue, 21 Dec 2010 10:20:33 +0100 |
haftmann |
only depend on exisiting statements
|
changeset |
files
|
| Tue, 21 Dec 2010 09:29:53 +0100 |
haftmann |
merged
|
changeset |
files
|
| Tue, 21 Dec 2010 09:29:33 +0100 |
haftmann |
evaluator separating static and dynamic operations
|
changeset |
files
|
| Tue, 21 Dec 2010 09:19:37 +0100 |
haftmann |
tuned naming
|
changeset |
files
|
| 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
|
| Mon, 20 Dec 2010 23:30:32 +0100 |
wenzelm |
updated to polyml-5.4.0;
|
changeset |
files
|
| Mon, 20 Dec 2010 23:26:17 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 20 Dec 2010 23:19:16 +0100 |
wenzelm |
updated for Poly/ML 5.4.0;
|
changeset |
files
|
| 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
|