Moved rewriting functions from Thm to MetaSimplifier.

- Moved rewriting functions to meta_simplifier.ML - dest_abs now also takes an optional variable name as an argument - beta_conversion takes additional flag as an argument. Fully reduces the term if set to true Some tuning: - tuned fix_shyps in instantiate, implies_intr, implies_elim, reflexive, transitive, beta_conversion, abstract_rule - combination: chktypes derives types of f and t from type of == instead of using fastype_of New primitives: - eta_conversion - incr_indexes: increment indexes in theorems - cterm_incr_indexes: increment indexes in cterms - cterm_match, cterm_first_order_match - rename_boundvars

moved rewriting functions from Drule to MetaSimplifier

- 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;

removed atomic_Trueprop (now in Pure/Isar/auto_bind.ML);

"atomize" for classical tactics;

atomize: all automated tactics that "solve" goals;

fixed two obscurities of "fix": predeclare_terms;

tuned names;

improved handling of "that": insert into goal, only declare as Pure "intro"; eliminated functor;

assumption / finish: handle non-atomic assumptions from context as well;

added atomic_judgment;

structure Obtain = Obtain;

new lemma card_Diff2_less for mulilated chess board

*** empty log message ***

*** empty log message ***

*** empty log message ***

the section command will belong to the new file

advanced induction examples