rearranged inductive package for Isar;

Generic inductive cases facility for (co)inductive definitions.

converted;

tuned;

tuned inductions;

prove: Envir.beta_norm;

new SList theory from Bu Wolff

induct: rule_versions produces localized variants;

empty rule_context for multiple goals;

added empty;

mutual rules declared as ``consumes 0'';

induct_atomize: include atomize_conj (for mutual induction);

Isar: 'induct' proper support for mutual induction involving non-atomic rule statements; Isar/Pure: support multiple simultaneous goal statements;

proper handling of mutual rules (esp. for sets);

lemmas induct_atomize = atomize_conj ...; val local_imp_def = thm "induct_implies_def";

val local_imp_def = thm "induct_implies_def";

ZF/Induct,UNITY

Tidying necessitated by new simprules in equalities.ML

conditional miniscoping equalities now made unconditional

new-style numerals without leading #, along with generic 0 and 1

congc now returns None if congruence rule has no effect.

Renamed some bound variables due to changes in simplifier.

Fixed proof depending on strange behaviour of rename_bvs.

Renamed some bound variables due to changes in simplifier.

present multi_result;

added meta_conjunction_tr';

pure_syntax_output: "_meta_conjunction";

adapted to multiple results;

adapted auto_bind_goal, auto_bind_facts;

added multi_theorem(_i); have, show etc.: multiple statements;