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;