Sun, 20 Oct 2013 19:20:08 +0200 blanchet tuning
Sun, 20 Oct 2013 19:20:08 +0200 blanchet tuning
Sun, 20 Oct 2013 19:20:08 +0200 blanchet tuning
Sun, 20 Oct 2013 18:22:59 +0200 blanchet simplify code
Sun, 20 Oct 2013 17:45:54 +0200 blanchet avoid tactic failure for equations that contain an unapplied 'id'
Sat, 19 Oct 2013 00:00:50 +0200 blanchet improve support for recursion through functions
Fri, 18 Oct 2013 20:26:46 +0200 blanchet handle composition for multiple arguments correctly
Fri, 18 Oct 2013 19:18:32 +0200 panny merge
Fri, 18 Oct 2013 19:03:39 +0200 panny generate callssss
Fri, 18 Oct 2013 18:58:46 +0200 blanchet set stage for more flexible 'primrec' syntax for recursion through functions
Fri, 18 Oct 2013 17:47:25 +0200 blanchet don't print BNF constants
Fri, 18 Oct 2013 16:02:07 +0200 blanchet tuning
Fri, 18 Oct 2013 15:42:55 +0200 blanchet conceal even more ugly constructions
Fri, 18 Oct 2013 15:25:39 +0200 blanchet conceal more ugly constructions
Fri, 18 Oct 2013 15:19:21 +0200 blanchet conceal prim(co)rec definitions
Fri, 18 Oct 2013 15:12:04 +0200 blanchet avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
Fri, 18 Oct 2013 15:00:40 +0200 blanchet updated docs
Fri, 18 Oct 2013 14:58:02 +0200 blanchet set code attribute on discriminator equations
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
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip