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;

tuned;

induct: cases are extracted from rulified rule;

removed obsolete make_raw;

lemma Least_mono moved from Typedef.thy to Set.thy;