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

normalize and postprocess proof body in a separate future, taking care of platforms without multithreading (greately improves parallelization in general without the overhead of promised proofs, cf. usedir -q 0);

merged

avoid store flag in add_* operations

arities: no need to maintain original codomain (cf. f795c1164708) -- completion happens in axclass.ML; misc tuning;

merged

do not expose store flag of AxClass.add_*

merged

adapted to changes

capitalized type variables; added yield as keyword