Fri, 20 Aug 2010 17:04:15 +0200 blanchet remove trivial facts
Fri, 20 Aug 2010 16:44:48 +0200 blanchet unbreak "only" option of Sledgehammer
Fri, 20 Aug 2010 16:28:53 +0200 blanchet merged
Fri, 20 Aug 2010 16:22:51 +0200 blanchet improve "x = A | x = B | x = C"-style axiom detection
Fri, 20 Aug 2010 15:56:00 +0200 blanchet temporarily disable "fequal" handling in Metis;
Fri, 20 Aug 2010 15:16:27 +0200 blanchet use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
Fri, 20 Aug 2010 14:18:55 +0200 blanchet merged
Fri, 20 Aug 2010 14:15:29 +0200 blanchet improve "x = A | x = B | x = C"-style fact discovery
Fri, 20 Aug 2010 14:09:02 +0200 blanchet transform elim theorems before filtering "bool" and "prop" variables out;
Fri, 20 Aug 2010 13:39:47 +0200 blanchet more fiddling with Sledgehammer's "add:" option
Fri, 20 Aug 2010 10:58:01 +0200 blanchet beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
Thu, 19 Aug 2010 19:34:11 +0200 blanchet generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
Thu, 19 Aug 2010 18:16:47 +0200 blanchet encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
Thu, 19 Aug 2010 14:39:31 +0200 blanchet fix atomize
Thu, 19 Aug 2010 14:01:54 +0200 blanchet improve atomization
Thu, 19 Aug 2010 13:04:37 +0200 blanchet fix SInE's error handling + run "vampire" locally if either SPASS or E is missing
Thu, 19 Aug 2010 12:04:07 +0200 blanchet added entries
Thu, 19 Aug 2010 12:03:47 +0200 blanchet update docs
Thu, 19 Aug 2010 11:30:48 +0200 blanchet tuning
Thu, 19 Aug 2010 11:30:32 +0200 blanchet parse SNARK proofs
Thu, 19 Aug 2010 11:29:53 +0200 blanchet added remote SInE and remote SNARK
Thu, 19 Aug 2010 11:02:59 +0200 blanchet no spurious trailing "\n" at the end of Sledgehammer's output
Wed, 18 Aug 2010 20:53:55 +0200 blanchet don't get confused by wrong slice
Wed, 18 Aug 2010 20:17:03 +0200 blanchet make sure that "add:" doesn't influence the relevance filter too much
Wed, 18 Aug 2010 19:57:12 +0200 blanchet tuning of relevance filter
Wed, 18 Aug 2010 18:01:54 +0200 blanchet minor cleanup
Wed, 18 Aug 2010 17:53:12 +0200 blanchet bound variables can be just as evil as schematic variables and lead to unsound proofs (e.g. "all_bool_eq")
Wed, 18 Aug 2010 17:23:17 +0200 blanchet update docs
Wed, 18 Aug 2010 17:16:37 +0200 blanchet get rid of "minimize_timeout", now that there's an automatic adaptive timeout mechanism in "minimize"
Wed, 18 Aug 2010 17:09:05 +0200 blanchet added "max_relevant_per_iter" option to Sledgehammer
Wed, 18 Aug 2010 16:42:37 +0200 blanchet thank Andrei instead of Tanya
Wed, 18 Aug 2010 16:39:05 +0200 blanchet fix the relevance filter so that it ignores If, Ex1, Ball, Bex
Wed, 18 Aug 2010 16:33:34 +0200 blanchet tuning
Fri, 20 Aug 2010 15:29:36 +0200 wenzelm reactivated -segprot options, just to make double-sure;
Sun, 22 Aug 2010 22:28:24 +0200 wenzelm tuned Markup_Tree.+ : slightly more expensive version to rebuild rest avoids crash of RedBlack.scala:120 (version Scala 2.8.0), e.g. on the following input:
Sun, 22 Aug 2010 22:09:14 +0200 wenzelm tuned;
Sun, 22 Aug 2010 20:25:15 +0200 wenzelm tuned signature;
Sun, 22 Aug 2010 20:11:17 +0200 wenzelm simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);
Sun, 22 Aug 2010 19:55:41 +0200 wenzelm proper range for hyperlinks and tooltips, using original markup information;
Sun, 22 Aug 2010 19:53:20 +0200 wenzelm tuned signature;
Sun, 22 Aug 2010 19:33:01 +0200 wenzelm misc tuning and simplification;
Sun, 22 Aug 2010 18:46:16 +0200 wenzelm renamed Markup_Tree.Node to Text.Info;
Sun, 22 Aug 2010 16:43:20 +0200 wenzelm removed obsolete Markup_Tree.flatten/filter;
Sun, 22 Aug 2010 16:37:15 +0200 wenzelm Isabelle_Hyperlinks: select relevant information directly from Markup_Tree, without intermediate RefInfo;
Sun, 22 Aug 2010 13:59:47 +0200 wenzelm Document_View.text_area_extension: select relevant information directly from Markup_Tree, without intermediate TypeInfo;
Sun, 22 Aug 2010 13:52:24 +0200 wenzelm tuned signatures;
Sun, 22 Aug 2010 12:54:12 +0200 wenzelm Command.State: accumulate markup reports uniformly;
Fri, 20 Aug 2010 22:35:01 +0200 wenzelm Markup_Tree.select: misc simplification, proper restriction of parent in subtree;
Fri, 20 Aug 2010 22:32:15 +0200 wenzelm added Text.Range.- convenience;
Fri, 20 Aug 2010 20:11:25 +0200 wenzelm tuned signatures;
Fri, 20 Aug 2010 12:12:28 +0200 wenzelm alternative constructor for Range singularities;
Fri, 20 Aug 2010 11:57:43 +0200 wenzelm concentrate protocol message formats in Isar_Document;
Fri, 20 Aug 2010 11:47:33 +0200 wenzelm Branches.overlapping: proper treatment of stop_range that overlaps with end;
Fri, 20 Aug 2010 11:00:15 +0200 wenzelm further clarification/unification of Position.Range and Text.Range concerning singularities: start offset is always included;
Thu, 19 Aug 2010 22:52:00 +0200 wenzelm parameterized type Markup_Tree.Node;
Thu, 19 Aug 2010 22:26:15 +0200 wenzelm added toString methods;
Thu, 19 Aug 2010 22:04:20 +0200 wenzelm misc tuning and simplification;
Thu, 19 Aug 2010 18:44:26 +0200 wenzelm updated some isatest settings;
Thu, 19 Aug 2010 18:19:21 +0200 wenzelm added generated file;
Thu, 19 Aug 2010 17:41:52 +0200 wenzelm merged
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip