handle "Id" gracefully w.r.t. "set"

reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature

handle "set" correctly in Refute -- inspired by old code from Isabelle2007

create consts with proper "set" types

tuned Refute

lower cardinality for faster testing

simplify mem Collect

tuning

ported Minipick to "set"

fixed set extensionality code

tuned import

construct correct "set" type for wf goal

fixed Nitpick's typedef handling w.r.t. "set"

fixed type annotations

rationalized output (a bit)

fixed a few more bugs in \Nitpick's new "set" support

regenerate SMT example certificates, to reflect "set" type constructor

port part of Nitpick to "set" type constructor

reintroduced failing examples now that they work again, after reintroduction of "set"

ported mono calculus to handle "set" type constructors

fixed spurious catch-all patterns

more benchmarks; tuned;

tuned

ported "Sets" example to "set" type constructor

ported a dozen of proofs to the "set" type constructor

reintroduced "metis" call taken out after reintroducing "set" as a constructor, and added two "metis" calls that used to be too slow

update docs to reflect "Manual_Nits"

removed special handling for set constants in relevance filter

reintroduced Sledgehammer call taken out by 9bc924006136, with some hints to guide the naive relevance filter

killed unfold_set_const option that makes no sense now that set is a type constructor again