Fri, 18 Oct 2013 13:38:55 +0200 blanchet MaSh error handling
Fri, 18 Oct 2013 13:30:09 +0200 blanchet repair invariant in MaSh when learning new proofs
Fri, 18 Oct 2013 10:43:21 +0200 blanchet killed more "no_atp"s
Fri, 18 Oct 2013 10:43:20 +0200 blanchet killed most "no_atp", to make Sledgehammer more complete
Fri, 18 Oct 2013 10:35:57 +0200 blanchet doc fixes suggested by Andreas L.
Fri, 18 Oct 2013 10:35:56 +0200 blanchet make sure that registered code equations are actually equations
Fri, 18 Oct 2013 10:35:55 +0200 blanchet accept very long lines in MaSh
Fri, 18 Oct 2013 00:05:31 +0200 blanchet make sure add: doesn't add duplicates, and works for [no_atp] facts
Thu, 17 Oct 2013 23:41:00 +0200 blanchet no fact subsumption -- this only confuses later code, e.g. 'add:'
Thu, 17 Oct 2013 20:49:19 +0200 blanchet generate a comment storing the goal nickname in "learn_prover"
Thu, 17 Oct 2013 20:20:53 +0200 blanchet clarified message
Thu, 17 Oct 2013 20:03:37 +0200 blanchet added thread-safety warnings
Thu, 17 Oct 2013 18:53:00 +0200 blanchet avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
Thu, 17 Oct 2013 18:53:00 +0200 blanchet handle nested tuples in 'let's
Thu, 17 Oct 2013 16:45:54 +0200 nipkow more exercises
Thu, 17 Oct 2013 13:37:13 +0200 blanchet also unfold let (_, _) = ... syntax
Thu, 17 Oct 2013 11:27:53 +0200 blanchet added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
Thu, 17 Oct 2013 10:29:28 +0200 blanchet graceful handling of abort
Thu, 17 Oct 2013 10:06:48 +0200 panny generalized interface
Thu, 17 Oct 2013 02:29:49 +0200 blanchet choose facts to reprove more randomly, to avoid getting stuck with impossible problems at first
Thu, 17 Oct 2013 02:22:54 +0200 blanchet thread the goal through instead of relying on unreliable (possibly fake) state
Thu, 17 Oct 2013 01:34:34 +0200 blanchet added comment
Thu, 17 Oct 2013 01:22:15 +0200 blanchet tuning
Thu, 17 Oct 2013 01:20:40 +0200 blanchet verbose minimization when learning from ATP proofs
Thu, 17 Oct 2013 01:10:08 +0200 blanchet if slicing is disabled, pick the maximum number of facts, not the number of facts in the last slice
Thu, 17 Oct 2013 01:04:00 +0200 blanchet if slicing is disabled, don't enforce last slice's "max_facts", but rather the maximum "max_facts"
Thu, 17 Oct 2013 01:03:59 +0200 blanchet fast track -- avoid domain error in 0 case
Thu, 17 Oct 2013 01:03:59 +0200 blanchet remove overloading of "max_facts" -- it already controls the number of facts passed to ATPs for 'learn_prover'
Wed, 16 Oct 2013 21:45:15 +0200 nipkow merged
Wed, 16 Oct 2013 21:44:56 +0200 nipkow tuned exercises
Wed, 16 Oct 2013 20:44:33 +0200 panny use Code.abort instead of undefined in auto-generated equations
Wed, 16 Oct 2013 19:55:23 +0200 blanchet have MaSh minimize
Tue, 15 Oct 2013 23:00:46 +0200 blanchet tweaked signature
Tue, 15 Oct 2013 22:55:01 +0200 blanchet strengthened tactic to deal with 'False ==> ...'
Tue, 15 Oct 2013 17:21:16 +0200 blanchet made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverse-engineering proof terms
Tue, 15 Oct 2013 16:14:52 +0200 blanchet improved duplicate detection in "build_name_tables" by ensuring that the earliest occurrence of a duplicate (if it exists) gets picked as the canonical instance
Tue, 15 Oct 2013 15:31:32 +0200 blanchet updated S/H docs
Tue, 15 Oct 2013 15:31:18 +0200 blanchet use MePo with Auto Sledgehammer, because it's lighter than MaSh and always available
Tue, 15 Oct 2013 15:26:58 +0200 blanchet drop only real duplicates, not subsumed facts -- this confuses MaSh
Tue, 15 Oct 2013 11:49:39 +0100 paulson renamed relcomp_def to relcomp_unfold
Tue, 15 Oct 2013 12:25:45 +0200 nipkow fixed thm names
Tue, 15 Oct 2013 10:59:34 +0200 blanchet addressed rare case where the same symbol would be treated alternately as a function and as a predicate -- adding "top2I top_boolI" to a problem that didn't talk about "top" was a way to trigger the issue
Mon, 14 Oct 2013 11:14:14 +0200 blanchet added Nitpick limitations to docs
Mon, 14 Oct 2013 11:07:59 +0200 blanchet more defensive Nitpick setup -- exotic types of recursion are not supported yet in the model finder
Mon, 14 Oct 2013 10:55:49 +0200 blanchet keep temporary error handling in there until code equations are properly generated
Mon, 14 Oct 2013 10:50:44 +0200 blanchet tuning (simplified parts of 92c5bd3b342d)
Mon, 14 Oct 2013 10:27:16 +0200 blanchet tuning
Mon, 14 Oct 2013 10:06:03 +0200 blanchet stengthened tactic to cope with abort cases
Mon, 14 Oct 2013 09:31:42 +0200 blanchet tuned names
Mon, 14 Oct 2013 09:17:04 +0200 blanchet strengthened tactic w.r.t. "let"
Sun, 13 Oct 2013 21:36:26 +0200 blanchet more prominent MaSh errors
Fri, 11 Oct 2013 23:15:30 +0200 panny compile -- fix typo introduced in 07a8145aaeba
Fri, 11 Oct 2013 20:47:37 +0200 panny pass the right theorems to tactic
Fri, 11 Oct 2013 16:31:23 +0200 panny prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
Thu, 10 Oct 2013 08:23:57 +0200 blanchet repaired confusion between the stated and effective fact filter -- the mismatch could result in "Match" exceptions
Thu, 10 Oct 2013 01:17:37 +0200 blanchet simplify fudge factor code
Wed, 09 Oct 2013 17:21:28 +0200 blanchet cleanup SMT-related config options
Wed, 09 Oct 2013 16:40:03 +0200 blanchet no isar proofs if preplay was not attempted
Wed, 09 Oct 2013 16:38:48 +0200 blanchet normalize more equalities
Wed, 09 Oct 2013 16:07:33 +0200 blanchet parallelize MeSh
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip