inductive_rulify2 accomodates malformed induction rules;

Sign.certify_tycon, Sign.certify_const;

improved cong_definition theorems; overloaded standard operations;

simplified induction;

added axclass power (from HOL.thy);

simplified atomize; added inductive_rulify2 (to accomodate malformed induction rules);

axclass power moved to Nat.thy;

added axclass inverse and consts inverse, divide (infix "/"); moved axclass power to Nat.thy;

FOL_basic_ss: simprocs moved to FOL_ss;

added atomize_eq;

val atomize = thms "atomize'";

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

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;