commented out vaporware

more exercises

tuning

tuning

tuned names (to make them independent from temporary naming convention used in characteristic theorems)

align 'primrec_new' on 'primcorec' (+ got rid of one more 'dummyT')

convenience: handle composition gracefully in map in 'primcorec', analogously to 'primrec_new'

tuned error message

more exercises

handle applied ctor arguments gracefully when computing 'callssss' (for recursion through functions)

tuning

more correct (!) types for recursive calls

watch out for 'case' constant canditates whose general type is 'a (e.g. 'undefined')

got rid of annoying duplicate rewrite rule warnings

use definitions for LEO-II as well -- this simplifies the code and matches some users' expectations

refactored rtrancl_while; prove termination for finite rtrancl

more exercises

added exercises

added 'primcorec' examples

tuned

removed junk

update doc according to c0186a0d8cb3

define a trivial nonemptiness witness if none is provided

made lower-level function available

more doc -- feedback from Andrei P.

added exercise

more docs

more docs

more docs

expand doc a bit

updated doc

tuning

warn about incompatible recursor signature

more informative abort

tuning

systematically close derivations in BNF package

removed temporary error handling

strengthened tactic

tuning

reintroduced parts of 07a8145aaeba that a22ded8a7f7d wrongly took out

tuning

gracefully handle case where a nested recursive variable appears directly on the rhs of a primcorec equation

tuning

tuning

tuning

tuning

simplify code

avoid tactic failure for equations that contain an unapplied 'id'

improve support for recursion through functions

handle composition for multiple arguments correctly

merge

generate callssss

set stage for more flexible 'primrec' syntax for recursion through functions

don't print BNF constants

tuning

conceal even more ugly constructions

conceal more ugly constructions

conceal prim(co)rec definitions

avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'

updated docs

set code attribute on discriminator equations

MaSh error handling

repair invariant in MaSh when learning new proofs

killed more "no_atp"s

killed most "no_atp", to make Sledgehammer more complete

doc fixes suggested by Andreas L.

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