| Mon, 10 Jan 2011 15:45:46 +0100 |
wenzelm |
eliminated Int.toString;
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 11:26:29 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 11:26:28 +0100 |
blanchet |
added Sledgehammer support for higher-order propositional reasoning
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 11:26:28 +0100 |
blanchet |
add Metis support for higher-order propositional reasoning
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 11:26:28 +0100 |
blanchet |
implemented partially-typed "tags" type encoding
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 12:49:05 +0200 |
blanchet |
prevent type errors because of inconsistent skolem Var types by giving fresh indices to Skolems
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 11:10:00 +0200 |
blanchet |
renaming
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 10:57:04 +0200 |
blanchet |
no need to encode theorem number twice in skolem names
|
file |
diff |
annotate
|
| Wed, 06 Oct 2010 17:44:07 +0200 |
blanchet |
qualify "Meson." and "Metis." constants so that the ML files can be reloaded later (e.g. for testing/development)
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 12:50:45 +0200 |
blanchet |
tuned comments
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 11:45:10 +0200 |
blanchet |
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
|
file |
diff |
annotate
|
| Mon, 04 Oct 2010 22:45:09 +0200 |
blanchet |
move Metis into Plain
|
file |
diff |
annotate
| base
|