implemented "mk_iter_or_rec_tac"

generate iter/rec goals

repaired constant types

some work towards iterator and recursor properties

tuning

correctly curry recursor arguments

added high-level recursor, not yet curried

merged

tuned proofs;

postpone update of text overview panel after incoming session edits, to improve reactivity of editing massive theories like src/HOL/Multivariate_Analysis;

more explicit Delay operations;

tuned proofs;

clearer names for functions in Quickcheck's narrowing engine

merged

tuned latex

lattice instances for option type

combinator Option.these

adjusted examples

countable_datatype method: pre-instantiate induction rule to avoid failure with e.g. datatype a = A "b list" and b = B "a"

handle type constructors not known to be a BNF using the DEADID BNF

respect order of/additional type variables supplied by the user in fixed point constructions;

gracefully handle shadowing case (fourth step of sugar localization)

careful about constructor types w.r.t. fake context (third step of localization)

read the real types off the constant types, rather than using the fake parser types (second step of sugar localization)

tuning

use "add_type" rather than "add_types_global"

don't throw away the context when hacking the theory (first step to localize the sugar code)

tuning

introduced and used "mk_Freesss", and simplified "mk_Freess(')"

construct high-level iterator RHS