merged

Hilbert_Classical: disable multithreading altogether, otherwise proof normalization will fork futures independently of Goal.parallel_proofs;

merged

added lemmas

merged

merge

fix parameter settings

merged

merged

update NEWS

fix Nitpick soundness bug regarding The and Eps

added examples/tests for THE and SOME

cosmetics

adapt example

fix code that used to raise an exception if bound variables were given a finite function type, because the old vs. new bound variable types were confused

improved precision of "set" based on an example from Lukas

remove debug output

removed "nitpick_intro" attribute -- Nitpick noew uses Spec_Rules instead

subsumed by NEWS -- for older history, see previous versions of Nitpick

don't show spurious "..." in Nitpick's output for free variables of set type (e.g., P (op +) example from Manual_Nits.thy); undoes parts of 38ba15040455, which was too aggressive

honor xsymbols in Nitpick

added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"

document new option

make Nitpick handle multiple typedef entries for same typedef

remove comment

thread along context instead of theory for typedef lookup

obsolete FIXME

move SAT solver warning from every invocation of SAT solver to the tool, Refute, that uses it; "size_change" rarely needs anything beyond "dpll", so this warning is annoying at best, and when "size_change" is called from Nitpick the warning confuses users, who then think that Nitpick is using "dpll" when it's really using MiniSat or some other fast solver

don't include any axioms for "TYPE" in Nitpick

dropped obsolete script