> etc

new: > and >=

rule inversion

JMB -> JMPB. Email von Johannes Pfeifroth.

updated;

fixed \title: convert "_" to "-";

tuned isabelle environment;

subgoals

*** empty log message ***

better discussion of rule induction

Thm.dest_abs now takes an additional argument.

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