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