| 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
|
| Wed, 08 Jun 2011 17:49:01 +0200 |
wenzelm |
updated headers;
|
changeset |
files
|
| Wed, 08 Jun 2011 17:42:07 +0200 |
wenzelm |
moved sources -- eliminated Netbeans artifact of jedit package directory;
|
changeset |
files
|
| Wed, 08 Jun 2011 17:32:31 +0200 |
wenzelm |
removed obsolete Netbeans project setup;
|
changeset |
files
|
| Wed, 08 Jun 2011 17:11:00 +0200 |
wenzelm |
support fresh build of jars;
|
changeset |
files
|
| Wed, 08 Jun 2011 16:19:22 +0200 |
wenzelm |
more jvmpath wrapping for Cygwin;
|
changeset |
files
|
| Wed, 08 Jun 2011 15:56:57 +0200 |
wenzelm |
more robust exception pattern General.Subscript;
|
changeset |
files
|
| Wed, 08 Jun 2011 15:39:55 +0200 |
wenzelm |
pervasive Output operations;
|
changeset |
files
|
| Wed, 08 Jun 2011 15:25:44 +0200 |
wenzelm |
modernized Proof_Context;
|
changeset |
files
|
| Wed, 08 Jun 2011 14:44:54 +0200 |
wenzelm |
standardized header;
|
changeset |
files
|
| Wed, 08 Jun 2011 13:45:01 +0200 |
boehmes |
merged
|
changeset |
files
|
| Wed, 08 Jun 2011 13:43:15 +0200 |
boehmes |
updated SMT certificates
|
changeset |
files
|
| Wed, 08 Jun 2011 11:59:45 +0200 |
boehmes |
only collect substituions neither seen before nor derived in the same refinement step
|
changeset |
files
|
| Wed, 08 Jun 2011 12:13:37 +0200 |
wenzelm |
updated imports (cf. 93b1183e43e5);
|
changeset |
files
|
| Wed, 08 Jun 2011 10:24:07 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
new Metis version
|
changeset |
files
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
|
changeset |
files
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
exploit new semantics of "max_new_instances"
|
changeset |
files
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
minor optimization
|
changeset |
files
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
don't needlessly extensionalize
|
changeset |
files
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
don't needlessly presimplify -- makes ATP problem preparation much faster
|
changeset |
files
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
tuned
|
changeset |
files
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
removed experimental code submitted by mistake
|
changeset |
files
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
|
changeset |
files
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
removed removed option from documentation
|
changeset |
files
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
killed "explicit_apply" option in Sledgehammer -- the "smart" default is about as lightweight as "false" and just as complete as "true"
|
changeset |
files
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
slightly faster/cleaner accumulation of polymorphic consts
|
changeset |
files
|
| Wed, 08 Jun 2011 00:01:20 +0200 |
krauss |
eliminated unnecessary tail-recursion and funny use of records as 'named arguments' for functions
|
changeset |
files
|
| Wed, 08 Jun 2011 00:01:20 +0200 |
krauss |
more conventional variable naming
|
changeset |
files
|
| Wed, 08 Jun 2011 00:01:20 +0200 |
krauss |
dropped outdated/speculative historical comments;
|
changeset |
files
|
| Wed, 08 Jun 2011 00:01:20 +0200 |
krauss |
less redundant tags
|
changeset |
files
|
| Wed, 08 Jun 2011 00:01:20 +0200 |
krauss |
removed generation of instantiated pattern set, which is never actually used
|
changeset |
files
|
| Wed, 08 Jun 2011 00:01:20 +0200 |
krauss |
more precise type for obscure "prfx" field
|
changeset |
files
|
| Tue, 07 Jun 2011 21:37:40 +0200 |
boehmes |
clarified (and slightly modified) the semantics of max_new_instances
|
changeset |
files
|
| Tue, 07 Jun 2011 19:22:52 +0200 |
kleing |
use null_heap instead of %_. 0 to avoid printing problems
|
changeset |
files
|
| Tue, 07 Jun 2011 14:38:42 +0200 |
blanchet |
prioritize more relevant facts for monomorphization
|
changeset |
files
|
| Tue, 07 Jun 2011 14:17:35 +0200 |
blanchet |
more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
|
changeset |
files
|
| Tue, 07 Jun 2011 14:17:35 +0200 |
blanchet |
workaround current "max_new_instances" semantics
|
changeset |
files
|
| Tue, 07 Jun 2011 14:17:35 +0200 |
blanchet |
fixed missing proof handling
|
changeset |
files
|
| Tue, 07 Jun 2011 14:17:35 +0200 |
blanchet |
optimized the relevance filter a little bit
|
changeset |
files
|
| Tue, 07 Jun 2011 14:06:12 +0200 |
bulwahn |
printing environment in mutabelle's log
|
changeset |
files
|
| Tue, 07 Jun 2011 11:24:54 +0200 |
bulwahn |
merged
|
changeset |
files
|
| Tue, 07 Jun 2011 11:24:16 +0200 |
bulwahn |
merged; manually merged IsaMakefile
|
changeset |
files
|
| Tue, 07 Jun 2011 11:12:05 +0200 |
bulwahn |
splitting Cset into Cset and List_Cset
|
changeset |
files
|
| Tue, 07 Jun 2011 11:11:01 +0200 |
bulwahn |
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
|
changeset |
files
|
| Tue, 07 Jun 2011 11:10:58 +0200 |
bulwahn |
adding examples with existentials
|
changeset |
files
|
| Tue, 07 Jun 2011 11:10:57 +0200 |
bulwahn |
renaming the formalisation of the birthday problem to a proper English name
|
changeset |
files
|
| Tue, 07 Jun 2011 11:10:42 +0200 |
bulwahn |
adding compilation that allows existentials in Quickcheck_Narrowing
|
changeset |
files
|