removed obsolete/unused pred_congs;

tuned comments;

converted ML proofs from simpdata.ML; tuned;

removed dead code;

RuleInsts.res_inst_tac with proper context;

more antiquotations;

tuned;

explicit rule for induct_tac

tuned spacing;

updated generated file;

* Attributes cases, induct, coinduct support del option.

added del attributes; tuned;

back to original import order -- thanks to proper deletion of nat cases/induct rules from type_definition;

proper deletion of nat cases/induct rules from type_definition;

fixed spelling (Where is WordExamples.thy anyway?);

recovered nat_induct as default for induct_tac;

more robust declaration of nat_induct;

reordering of imports ensures that nat_induct stay in front;

adhoc fix of induct_tac: rule nat_induct;

case_tac: accomodate change in bound variable name;

nat_induct_tac (works without context);

moved case_tac/induct_tac to induct_tacs.ML -- no longer hardwired into datatype package;

added nat_induct_tac (works without context);

InductTacs.case_tac with proper context and proper declaration of local variable;

added HOL/Tools/induct_tacs.ML;

eliminated obsolete case_split_thm -- use case_split; added case_split_tac (works without context); setup for induct_tacs.ML;

tuned proofs -- case_tac *is* available here;

updated generated file;