make sure that registered code equations are actually equations

accept very long lines in MaSh

make sure add: doesn't add duplicates, and works for [no_atp] facts

no fact subsumption -- this only confuses later code, e.g. 'add:'

generate a comment storing the goal nickname in "learn_prover"

clarified message

added thread-safety warnings

avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk

handle nested tuples in 'let's

more exercises

also unfold let (_, _) = ... syntax

added helper function (that solves chicken-and-egg problem w.r.t. "callssss")

graceful handling of abort

generalized interface

choose facts to reprove more randomly, to avoid getting stuck with impossible problems at first

thread the goal through instead of relying on unreliable (possibly fake) state

added comment

tuning

verbose minimization when learning from ATP proofs

if slicing is disabled, pick the maximum number of facts, not the number of facts in the last slice

if slicing is disabled, don't enforce last slice's "max_facts", but rather the maximum "max_facts"

fast track -- avoid domain error in 0 case

remove overloading of "max_facts" -- it already controls the number of facts passed to ATPs for 'learn_prover'

merged

tuned exercises

use Code.abort instead of undefined in auto-generated equations

have MaSh minimize

tweaked signature

strengthened tactic to deal with 'False ==> ...'

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

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

updated S/H docs

use MePo with Auto Sledgehammer, because it's lighter than MaSh and always available

drop only real duplicates, not subsumed facts -- this confuses MaSh

renamed relcomp_def to relcomp_unfold

fixed thm names

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

added Nitpick limitations to docs

more defensive Nitpick setup -- exotic types of recursion are not supported yet in the model finder

keep temporary error handling in there until code equations are properly generated

tuning (simplified parts of 92c5bd3b342d)

tuning

stengthened tactic to cope with abort cases

tuned names

strengthened tactic w.r.t. "let"

more prominent MaSh errors

compile -- fix typo introduced in 07a8145aaeba

pass the right theorems to tactic

prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.; generate code-style theorems (currently commented out since this still fails for many cases); filter tautologies (False ==> ...) out of generated theorems;

repaired confusion between the stated and effective fact filter -- the mismatch could result in "Match" exceptions

simplify fudge factor code

cleanup SMT-related config options

no isar proofs if preplay was not attempted

normalize more equalities

parallelize MeSh

run relevance filter only once for ATPs and SMT solvers, since it should now yield the same results anyway

use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)

minor performance tuning

use plain types instead of dedicated type pattern

duplicate term and type patterns

optimized built-in const check

added TODO

crank up limit a bit -- truly huge background theories are still nearly 3 times larger

higher minimum relevance threshold, to prevent Sledgehammer from taking too long on "lemma False"

minor fact filter speedups

more gracefully handle huge theories in relevance filters

handle huge MaSh requests gracefully

further optimization in relevance filter

further speed up duplicate elimination

more efficient theorem variable normalization

strengthened constructor-view tactic to deal with 'let's

allow 'let's around constructors in constructor view

reword abstract

more primcorec docs

minor doc fix

new topological lemmas; tuned proofs

strengthen the tactics to bring them in sync with the simplifications taking place in the code (and weaken the simplifications a bit -- let's not deal with implies)

generate optimized DNF formula

rationalized negation code

honor externally set MASH_PORT

process code-style inputs

more tracing

more thorough spying

more Sledgehammer spying -- record fact indices

prevent explosion in monomorphizer (e.g. when the facts typerep_int_def typerep_num_def typerep_option_def typerep_node_def are selected)

removed pointless special case

run fewer provers in "try" mode

count remote threads as well when balancing CPU usage -- otherwise jEdit users and other users of the "blocking" mode may have to wait for 2 * timeout if they e.g. have 4 cores and 5 provers (the typical situation)

more parallelism in blocking mode

more robustness in MaSh

back to post-release mode -- after fork point;

tuned;

tuned;

more notes;

tuned;

added and generalised lemmas

Streamlined locales reference material.

merged

tuned

merged

keep the qualification of bindings when noting bnf theorems

strengthened tactic (primcorec_sel_tac) + tuning

renamings

got rid of needless argument

make SMT integration slacker w.r.t. bad apples (facts)

strengthen top sort check

tuned whitespace;

tuned;

unset XMODIFIERS by default, in order to prevent total loss of key events seen on Fedora 18/19;

updated to scala-2.10.3;

tuned;

some highlights of Isabelle2013-1 based on NEWS;