not working yet. partial conversion to use "rename" instead of "extend"

new theorems inj_iff, surj_iff

new reference korf85

* Pure now provides its own version of intro/elim/dest attributes; useful for building new logics, but beware of confusion with the Provers/classical ones! * HOL: removed "case_split" thm binding, should use "cases" proof method anyway; * tuned syntax of "induct" method; * new "cases" method for propositions, inductive sets and types; * HOL/records: admit "r" as field name;

tuned syntax wrapper;

tuned "induct" syntax;

"cases" method;

added cases_tac;

induct: tuned syntax; added cases method;

added cases_of, cases;