don't generate code in Word because it breaks the current code setup

robustly parse Z3 4.0's output (with outcome appearing on first rather than last line)

added "Collect_cong" to cover extensionality of "Collect" (special cases of "ext" pass through the relevant filter)

remove the generation of a code certificate from the Quotient package (mainly from quotient_def), because it's in lift_definition now

generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command

infrastructure that makes possible to prove that a relation is reflexive

temporarily disable "ext" rule helpers until Metis supports them (and until they are properly evaluated)

lower skolem penalty to ensure that some useful facts with existentials, e.g. congruence of "setsum", eventually get picked up

treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect

get ready for automatic generation of extensionality helpers