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;

case_tac/induct_tac: use same declarations as cases/induct;

proper news header; methods case_tac and induct_tac now refer to usual declarations; removed obsolete induct_tac and thm_induct_tac;

removed obsolete read_idents;

added (e)res_inst_tac; tuned comments;

focus: actually declare constraints for local parameters;

tuned proofs;

case_split_tac (works without context);

tuned;

eliminated obsolete case_split_thm -- use case_split;

Unstructured induction and cases analysis for Isabelle/HOL.

dropped instance with attached definitions

polished interface of datatype package

adjusted some proofs involving inats

refactoring; addition, numerals