- new theorems imp_cong and swap_prems_eq - new function dest_equals - exported strip_imp_concl - removed incr_indexes (now in Thm)

Added new file meta_simplifier.ML

Moved meta simplification stuff from Thm to MetaSimplifier.

Added type constraint in theorem "lift".

*** empty log message ***

method 'induct' now handles non-atomic goals; improved error message; option 'stripped' deprecated;

improved: 'induct' handle non-atomic goals;

make: open_parms argument;

RuleCases.make true;

added rewrite_goal_tac; resolveq_cases_tac: generalized args; tuned atomize; assm_tac: include reflexive_thm;

added typ_instance;

Sign.typ_instance;

inductive_atomize, inductive_rulify;

* Isar/HOL: method 'induct' now handles non-atomic goals; as a consequence, it is no longer monotonic wrt. the local goal context (which is now passed through the inductive cases);

tuned atomize_goal;

minor modifications for new Springer style

minor changes

auto update

*** empty log message ***

updated;

tuned method "rule" and "default";

isamarkup: handle % in input;

tuned;

misc stuff;

tuned;

proper setup of "parallel"; removed unused rules;

tuned notation;

adapted "obtain" proofs;

provide case names for rev_induct, rev_cases;

rev_exhaust: rulify;