BV and LBV specified in terms of app and step functions

instantiated Cancel_Numerals for "nat" in ZF

more cterm operations: mk_implies, list_implies

prove_conv gets an extra argument, so the ZF instantiation can use hyps

tidied

added a dummy "thm list" argument to prove_conv for the new interface to Cancel_Numerals

new abstract syntax operations, used in ZF

ZF arith

*** empty log message ***

dummy_patterns moved to term.ML;

added goal_args('); added "cut_tac", "thin_tac", "rename_tac"; renamed inst tactics; inst syntax: include empty inst;

added int;

axioms: Term.no_dummy_patterns;

added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;

added rename_params_tac;

dummy_pattern moved to term.ML;

Term.no_dummy_patterns;

added rev_eq_reflection; export stac; proof method setup: subst, hypsubst;

val rev_eq_reflection = def_imp_eq;

val atomize = thms "atomize";

lemmas atomize = all_eq imp_eq; setup hypsubst_setup;

rev_eq_reflection = meta_eq_to_obj_eq;

removed stac (now exported by HypsubstFun);

setup hypsubst_setup;