- Equivariance simpset used in proofs of strong induction and inversion rules now contains perm_simproc_app and perm_simproc_fun as well - first_order_matchs now eta-contracts terms before matching - Rewrote code for proving strong inversion rule to avoid failure when one of the arguments of the inductive predicate has an atom type

pprint: back to proper output of markup, with workaround for Poly/ML crash;

back to 1.36 (Poly/ML crash!?);

updated generated file;

YXML: no special treatment of white space;

pprint: proper output of markup (important for token translation);

ml_code_antiq: proper scanner combinators; ML_Antiquote.value;

moved concrete antiquotations to ml_antiquote.ML;

Antiquote.Open/Close;

add_antiq: more general notion of ML antiquotation; eval_antiquotes: support blocks and background context; moved concrete antiquotations to ml_antiquote.ML;

added Open/Close -- checked blocks;

added pprint_thy_ref;

Common ML antiquotations.

added ML/ml_antiquote.ML;

ML_Antiquote.value;

added isaantiqopen/close;

Logic.all/mk_equals/mk_implies; Term.all;

moved implies to logic.ML; removed equals; qualified all;

added all, is_all; improved dest_all; added implies (from term.ML);

Logic.implies;

Logic.is_all;

Term.all;

Logic.all/mk_equals/mk_implies;

session name: empty for Pure and by default;

induct_tac: allow omission of arguments;

info: default name is "", not "Pure";

moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;

removed obsolete dest_concls;

induct_tac: mutual rules work as for method "induct";

tuned get_inductT: *all* rules for missing instantiation; exported get_inductT;