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