added a progress lemma and tuned some comments

* Rules and tactics that read instantiations now demand a proper context;

added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML); pervasive operations; tuned;

renamed rename_params_tac to rename_tac;

removed obsolete global instantiation tactics (cf. Isar/rule_insts.ML); removed obsolete rename_tac, rename_last_tac; renamed rename_params_tac to rename_tac;

removed obsolete no_qed, quick_and_dirty_prove_goalw_cterm; removed obsolete abbreviations for ML tactic scripts;

removed obsolete global read_insts/read_instantiate (cf. Isar/rule_insts.ML);

inst1_tac: proper context;

pervasive RuleInsts;

updated generated file;

converted ML proofs;

added read_instantiate;

ML tactic: do not abstract over context again;

export eof;

removed obsolete inst;

atomize: proper context; RuleInsts.read_instantiate;

atomize: proper context;

RuleInsts.read_instantiate;

ptac/prolog_tac: proper context;

allE_Nil: only one copy, proven in regular theory source;

deriv_tac/DERIV_tac: proper context;

sum3_instantiate: proper context;

eliminated OldGoals.inst;

updated generated file;

method "tactic": only "facts" as bound value; added method "raw_tactic";

Export a wrapper for all semiring_normalizers

proper context for tactics derived from res_inst_tac;

added ~: and ~=; fixed SOME, which is now \<some> not \<epsilon>;

export subgoal_tac, subgoals_tac, thin_tac;

prove: full Variable.declare_term, including constraints;