| Thu, 09 Jun 2011 00:16:28 +0200 |
blanchet |
renamed "untyped_aconv" to distinguish it clearly from the standard "aconv_untyped"
|
changeset |
files
|
| Wed, 08 Jun 2011 22:13:49 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 08 Jun 2011 17:01:07 +0200 |
blanchet |
avoid duplicate facts, which confuse the minimizer output
|
changeset |
files
|
| Wed, 08 Jun 2011 16:20:19 +0200 |
blanchet |
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
|
changeset |
files
|
| Wed, 08 Jun 2011 16:20:18 +0200 |
blanchet |
restore comment about subtle issue
|
changeset |
files
|
| Wed, 08 Jun 2011 16:20:18 +0200 |
blanchet |
made "query" type systes a bit more sound -- local facts, e.g. the negated conjecture, may make invalid the infinity check, e.g. if we are proving that there exists two values of an infinite type, we can use the negated conjecture that there is only one value to derive unsound proofs unless the type is properly encoded
|
changeset |
files
|
| Wed, 08 Jun 2011 16:20:18 +0200 |
blanchet |
don't launch the automatic minimizer for zero facts
|
changeset |
files
|
| Wed, 08 Jun 2011 16:20:18 +0200 |
blanchet |
don't generate unsound proof error for missing proofs
|
changeset |
files
|
| Wed, 08 Jun 2011 16:20:18 +0200 |
blanchet |
renamed option to avoid talking about seconds, since this is now the default Isabelle unit
|
changeset |
files
|
| Wed, 08 Jun 2011 16:20:18 +0200 |
blanchet |
fixed format selection logic for Waldmeister
|
changeset |
files
|
| Wed, 08 Jun 2011 16:20:18 +0200 |
blanchet |
better default type system for Waldmeister, with fewer predicates (for types or type classes)
|
changeset |
files
|
| Wed, 08 Jun 2011 22:06:05 +0200 |
wenzelm |
simplified directory structure;
|
changeset |
files
|
| Wed, 08 Jun 2011 21:40:54 +0200 |
wenzelm |
simplified directory structure;
|
changeset |
files
|
| Wed, 08 Jun 2011 21:29:49 +0200 |
wenzelm |
further jedit build option;
|
changeset |
files
|
| Wed, 08 Jun 2011 20:58:51 +0200 |
wenzelm |
build jedit as part of regular startup script (in that case depending on jedit_build component);
|
changeset |
files
|