generalized induct_scheme method to prove conditional induction schemes.

add lemma iterate_iterate

* Disposed old term read functions;

replace preorder class with locale

add lemma compact_imp_principal to locale ideal_completion

added type_constraint (formerly in type_infer.ML, which is now loaded later);

TypeExt.type_constraint;

simplified TypeInfer.infer_types;

improved error output -- variant/mark bounds; simplified infer_types -- always freeze, no result substitution;

load type_infer.ML after Syntax module;

eliminated old Sign.read_term/Thm.read_cterm etc.;

moved ProofContext.pretty_proof to ProofSyntax.pretty_proof; read_term: imitate old behaviour (allow_dummies, mode_schematic);

export transfer_syntax; added allow_dummies feature (for legacy emulations); moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;

moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;

removed obsolete term reading operations (cf. old_goals.ML for legacy emulations);

added emulations for simple_read_term/read_term/read_prop (formerly in sign.ML);

removed obsolete read_def_cterms/read_cterm;

load proof term operations later;

more antiquotations;

OldGoals.read_prop;

OldGoals.simple_read_term;

simplified Abel_Cancel setup;

updated generated file;

pervasive cut_inst_tac;