- 'induct' may now use elim-style induction rules without chaining facts, using ``missing'' premises from the goal state; this allows rules stemming from inductive sets to be applied in unstructured scripts, while still benefitting from proper handling of non-atomic statements; NB: major inductive premises need to be put first, all the rest of the goal is passed through the induction;

(induct set: ...);

put_consumes: really overwrite existing tag;

finish_global: Tactic.norm_hhf;

use HOL.induct_XXX;

use induct_rulify2;

renamed inductive_XXX to induct_XXX; added induct_impliesI;

induct_impliesI;

tuned induct proofs;

- 'induct' method now derives symbolic cases from the *rulified* rule (before it used to rulify cases stemming from the internal atomized version); this means that the context of a non-atomic statement becomes is included in the hypothesis, avoiding the slightly cumbersome show "PROP ?case" form;