| Thu, 14 Apr 2011 11:24:04 +0200 |
blanchet |
improve definitional CNF on goal by moving "not" past the quantifiers
|
file |
diff |
annotate
|
| Thu, 14 Apr 2011 11:24:04 +0200 |
blanchet |
experiment with definitional CNF
|
file |
diff |
annotate
|
| Thu, 14 Apr 2011 11:24:04 +0200 |
blanchet |
try to repair out-of-sync situations in Metis
|
file |
diff |
annotate
|
| Thu, 07 Apr 2011 12:16:25 +0200 |
blanchet |
tuned comment
|
file |
diff |
annotate
|
| Sat, 26 Mar 2011 15:55:22 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 24 Mar 2011 17:49:27 +0100 |
blanchet |
avoid evil "export_without_context", which breaks if there are local "fixes"
|
file |
diff |
annotate
|
| Thu, 24 Mar 2011 17:49:27 +0100 |
blanchet |
more robust handling of variables in new Skolemizer
|
file |
diff |
annotate
|
| Thu, 24 Mar 2011 16:56:19 +0100 |
wenzelm |
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
|
file |
diff |
annotate
|
| Wed, 23 Mar 2011 10:18:42 +0100 |
blanchet |
avoid illegal variable names, which then yield "Not an identifier" errors in "rename_tac"
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 13:45:43 +0100 |
wenzelm |
refer to regular structure Simplifier;
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 12:49:05 +0200 |
blanchet |
restructure Skolemization code slightly
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 12:49:05 +0200 |
blanchet |
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 12:49:05 +0200 |
blanchet |
more work on new Skolemizer without Hilbert_Choice
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 12:49:05 +0200 |
blanchet |
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
|
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 10:59:12 +0200 |
blanchet |
got rid of overkill "meson_choice" attribute;
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 10:30:50 +0200 |
blanchet |
more explicit name
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 10:28:11 +0200 |
blanchet |
factor out "Meson_Tactic" from "Meson_Clausify"
|
file |
diff |
annotate
|
| Mon, 04 Oct 2010 21:49:07 +0200 |
blanchet |
move Meson to Plain
|
file |
diff |
annotate
|
| Mon, 04 Oct 2010 21:37:42 +0200 |
blanchet |
move MESON files together
|
file |
diff |
annotate
| base
|