2008-06-18 ago wenzelm simplified TypeInfer.infer_types;
2008-06-18 ago wenzelm improved error output -- variant/mark bounds;
2008-06-18 ago wenzelm load type_infer.ML after Syntax module;
2008-06-18 ago wenzelm eliminated old Sign.read_term/Thm.read_cterm etc.;
2008-06-18 ago wenzelm moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
2008-06-18 ago wenzelm export transfer_syntax;
2008-06-18 ago wenzelm moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
2008-06-18 ago wenzelm removed obsolete term reading operations (cf. old_goals.ML for legacy emulations);
2008-06-18 ago wenzelm added emulations for simple_read_term/read_term/read_prop (formerly in sign.ML);
2008-06-18 ago wenzelm removed obsolete read_def_cterms/read_cterm;
2008-06-18 ago wenzelm load proof term operations later;
2008-06-18 ago wenzelm more antiquotations;
2008-06-18 ago wenzelm OldGoals.read_prop;
2008-06-18 ago wenzelm OldGoals.simple_read_term;
2008-06-18 ago wenzelm simplified Abel_Cancel setup;
2008-06-18 ago wenzelm updated generated file;
2008-06-18 ago wenzelm pervasive cut_inst_tac;
2008-06-17 ago urbanc added a progress lemma and tuned some comments
2008-06-16 ago wenzelm * Rules and tactics that read instantiations now demand a proper context;
2008-06-16 ago wenzelm added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
2008-06-16 ago wenzelm renamed rename_params_tac to rename_tac;
2008-06-16 ago wenzelm removed obsolete global instantiation tactics (cf. Isar/rule_insts.ML);
2008-06-16 ago wenzelm removed obsolete no_qed, quick_and_dirty_prove_goalw_cterm;
2008-06-16 ago wenzelm removed obsolete global read_insts/read_instantiate (cf. Isar/rule_insts.ML);
2008-06-16 ago wenzelm inst1_tac: proper context;
2008-06-16 ago wenzelm pervasive RuleInsts;
2008-06-16 ago wenzelm updated generated file;
2008-06-16 ago wenzelm converted ML proofs;
2008-06-16 ago wenzelm added read_instantiate;
2008-06-16 ago wenzelm ML tactic: do not abstract over context again;
2008-06-16 ago wenzelm export eof;
2008-06-16 ago wenzelm removed obsolete inst;
2008-06-16 ago wenzelm atomize: proper context;
2008-06-16 ago wenzelm atomize: proper context;
2008-06-16 ago wenzelm RuleInsts.read_instantiate;
2008-06-16 ago wenzelm ptac/prolog_tac: proper context;
2008-06-16 ago wenzelm allE_Nil: only one copy, proven in regular theory source;
2008-06-16 ago wenzelm deriv_tac/DERIV_tac: proper context;
2008-06-16 ago wenzelm sum3_instantiate: proper context;
2008-06-16 ago wenzelm eliminated OldGoals.inst;
2008-06-16 ago wenzelm updated generated file;
2008-06-16 ago wenzelm method "tactic": only "facts" as bound value;
2008-06-16 ago chaieb Export a wrapper for all semiring_normalizers
2008-06-14 ago wenzelm proper context for tactics derived from res_inst_tac;
2008-06-14 ago wenzelm added ~: and ~=;
2008-06-14 ago wenzelm export subgoal_tac, subgoals_tac, thin_tac;
2008-06-14 ago wenzelm prove: full Variable.declare_term, including constraints;
2008-06-14 ago wenzelm prove_standard: more precises argument passing;
2008-06-14 ago wenzelm InductTacs.case_tac: removed obsolete declare, which is now part of Goal.prove;
2008-06-14 ago wenzelm simplified InductTacs.case_tac/induct_tac;
2008-06-14 ago wenzelm tuned proof;
2008-06-14 ago wenzelm removed obsolete nat_induct_tac -- cannot work without;
2008-06-14 ago wenzelm removed obsolete case_split_tac -- cannot work without;
2008-06-14 ago wenzelm removed unused excluded_middle_tac;
2008-06-14 ago wenzelm updated geenrated file;
2008-06-14 ago wenzelm qualified old res_inst_tac variants;
2008-06-14 ago wenzelm proper context for tactics derived from res_inst_tac;
2008-06-14 ago wenzelm updated generated file;
2008-06-14 ago wenzelm obsolete;
2008-06-14 ago wenzelm certify_term: reject qualified frees;