Thu, 09 Jun 2011 08:32:21 +0200 bulwahn removing unneccessary manual instantiations and dead definitions; hiding more constants and facts
Thu, 09 Jun 2011 08:32:19 +0200 bulwahn adding a nicer error message for quickcheck_narrowing; hiding fact empty_def
Thu, 09 Jun 2011 08:32:18 +0200 bulwahn adding narrowing engine for existentials
Thu, 09 Jun 2011 08:32:18 +0200 bulwahn adapting Quickcheck_Narrowing: adding setup for characters; correcting import statement
Thu, 09 Jun 2011 08:32:16 +0200 bulwahn adding theory Quickcheck_Narrowing to HOL-Main image
Thu, 09 Jun 2011 08:32:15 +0200 bulwahn adapting IsaMakefile
Thu, 09 Jun 2011 08:32:14 +0200 bulwahn moving Quickcheck_Narrowing from Library to base directory
Thu, 09 Jun 2011 08:32:13 +0200 bulwahn compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
Thu, 09 Jun 2011 08:31:41 +0200 bulwahn local simp rule in List_Cset
Thu, 09 Jun 2011 00:16:28 +0200 blanchet tuning
Thu, 09 Jun 2011 00:16:28 +0200 blanchet compile
Thu, 09 Jun 2011 00:16:28 +0200 blanchet cleaner fact freshening, which also works in corner cases, e.g. if two backquoted facts have the same name (but have different variable indices)
Thu, 09 Jun 2011 00:16:28 +0200 blanchet added a really fully typed translation as a fallback for Metis, in rare cases where Metis correctly proves a theorem but has type-unsound steps in it (which is likelier to happen with some of the lighter translations)
Thu, 09 Jun 2011 00:16:28 +0200 blanchet improve sort inference in Metis proofs -- in some rare cases Metis steals Isabelle's variable names and the sorts must then be inferred as well
Thu, 09 Jun 2011 00:16:28 +0200 blanchet removed needless function that duplicated standard functionality, with a little unnecessary twist
Thu, 09 Jun 2011 00:16:28 +0200 blanchet removed more dead code
Thu, 09 Jun 2011 00:16:28 +0200 blanchet be a bit more liberal with respect to the universal sort -- it sometimes help
Thu, 09 Jun 2011 00:16:28 +0200 blanchet renamed "untyped_aconv" to distinguish it clearly from the standard "aconv_untyped"
Wed, 08 Jun 2011 22:13:49 +0200 wenzelm merged
Wed, 08 Jun 2011 17:01:07 +0200 blanchet avoid duplicate facts, which confuse the minimizer output
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
Wed, 08 Jun 2011 16:20:18 +0200 blanchet restore comment about subtle issue
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
Wed, 08 Jun 2011 16:20:18 +0200 blanchet don't launch the automatic minimizer for zero facts
Wed, 08 Jun 2011 16:20:18 +0200 blanchet don't generate unsound proof error for missing proofs
Wed, 08 Jun 2011 16:20:18 +0200 blanchet renamed option to avoid talking about seconds, since this is now the default Isabelle unit
Wed, 08 Jun 2011 16:20:18 +0200 blanchet fixed format selection logic for Waldmeister
Wed, 08 Jun 2011 16:20:18 +0200 blanchet better default type system for Waldmeister, with fewer predicates (for types or type classes)
Wed, 08 Jun 2011 22:06:05 +0200 wenzelm simplified directory structure;
Wed, 08 Jun 2011 21:40:54 +0200 wenzelm simplified directory structure;
Wed, 08 Jun 2011 21:29:49 +0200 wenzelm further jedit build option;
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);
Wed, 08 Jun 2011 17:49:01 +0200 wenzelm updated headers;
Wed, 08 Jun 2011 17:42:07 +0200 wenzelm moved sources -- eliminated Netbeans artifact of jedit package directory;
Wed, 08 Jun 2011 17:32:31 +0200 wenzelm removed obsolete Netbeans project setup;
Wed, 08 Jun 2011 17:11:00 +0200 wenzelm support fresh build of jars;
Wed, 08 Jun 2011 16:19:22 +0200 wenzelm more jvmpath wrapping for Cygwin;
Wed, 08 Jun 2011 15:56:57 +0200 wenzelm more robust exception pattern General.Subscript;
Wed, 08 Jun 2011 15:39:55 +0200 wenzelm pervasive Output operations;
Wed, 08 Jun 2011 15:25:44 +0200 wenzelm modernized Proof_Context;
Wed, 08 Jun 2011 14:44:54 +0200 wenzelm standardized header;
Wed, 08 Jun 2011 13:45:01 +0200 boehmes merged
Wed, 08 Jun 2011 13:43:15 +0200 boehmes updated SMT certificates
Wed, 08 Jun 2011 11:59:45 +0200 boehmes only collect substituions neither seen before nor derived in the same refinement step
Wed, 08 Jun 2011 12:13:37 +0200 wenzelm updated imports (cf. 93b1183e43e5);
Wed, 08 Jun 2011 10:24:07 +0200 wenzelm merged
Wed, 08 Jun 2011 08:47:43 +0200 blanchet new Metis version
Wed, 08 Jun 2011 08:47:43 +0200 blanchet removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
Wed, 08 Jun 2011 08:47:43 +0200 blanchet exploit new semantics of "max_new_instances"
Wed, 08 Jun 2011 08:47:43 +0200 blanchet minor optimization
Wed, 08 Jun 2011 08:47:43 +0200 blanchet don't needlessly extensionalize
Wed, 08 Jun 2011 08:47:43 +0200 blanchet don't needlessly presimplify -- makes ATP problem preparation much faster
Wed, 08 Jun 2011 08:47:43 +0200 blanchet tuned
Wed, 08 Jun 2011 08:47:43 +0200 blanchet removed experimental code submitted by mistake
Wed, 08 Jun 2011 08:47:43 +0200 blanchet make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
Wed, 08 Jun 2011 08:47:43 +0200 blanchet removed removed option from documentation
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"
Wed, 08 Jun 2011 08:47:43 +0200 blanchet slightly faster/cleaner accumulation of polymorphic consts
Wed, 08 Jun 2011 00:01:20 +0200 krauss eliminated unnecessary tail-recursion and funny use of records as 'named arguments' for functions
Wed, 08 Jun 2011 00:01:20 +0200 krauss more conventional variable naming
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip