removed duplicate lemma

adding two more examples to example theory

handling function types more carefully than in e98a06145530

adding order on modes

removing obsolete argument in prepare_intrs; passing context instead of theory in prepare_intrs

type antiquotation: allow arbitrary type abbreviations, but fail with user-space exception on bad input

merged

added Imperative HOL overview

print mode for Imperative HOL overview; tuned and more accurate dependencies

'class' and 'type' are now antiquoations by default

merged

merged

renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI

added and renamed lemmas

merged

directly computing the values of interest instead of composing functions in an unintelligent way that causes exponential much garbage; using the latest theory

added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet

use eta-contracted version for occurrence check (avoids possible non-termination) Test case: lemma "fwrap f = (%v. f v) ==> P f" apply clarify; pointed out by Thomas Sewell

tuned signature; tuned comments;

Type_Infer.finish: index 0 -- freshness supposedly via Name.invents; Type_Infer.fixate_params: full Proof.context;

simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;

tuned;

Type_Infer.preterm: eliminated separate Constraint;

Type_Infer.infer_types: plain error instead of kernel exception TYPE;

load type_infer.ML later -- proper context for Type_Infer.infer_types; renamed Type_Infer.polymorphicT to Type.mark_polymorphic;

common Type.appl_error, which also covers explicit constraints;

eliminated aliases of Type.constraint;

tuned;

tuned messages; tuned comments;

avoid extra wrapping for interrupts;