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;

tuned;