2007-07-03 ago moved (asm_)rewrite_goal_tac from goal.ML to meta_simplifier.ML (no longer depends on SELECT_GOAL);
2007-06-19 ago balanced conjunctions;
2007-06-18 ago tuned conjunction tactics: slightly smaller proof terms;
2007-06-13 ago renamed prove_raw to prove_internal;
2007-06-04 ago added assume_rule_tac;
2007-05-10 ago moved some Drule operations to Thm (see more_thm.ML);
2006-12-07 ago reorganized structure Goal vs. Tactic;
2006-11-30 ago added norm/close_result (supercede local_standard etc.);
2006-11-29 ago COMP_INCR;
2006-11-24 ago ProofContext.init;
2006-08-02 ago normalized Proof.context/method type aliases;
2006-07-30 ago Thm.adjust_maxidx;
2006-07-29 ago prove: proper assumption context, more tactic arguments;
2006-07-27 ago moved Goal.norm_hhf(_protect) to meta_simplifier.ML (pervasive);
2006-07-19 ago prove: Variable.declare_internal (more efficient);
2006-07-08 ago prove/prove_multi: context;
2006-06-12 ago Unify.matches_list;
2006-06-05 ago allow non-trivial schematic goals (via embedded term vars);
2006-05-11 ago check result against certified prop, i.e. admit non-normal statements;
2006-04-27 ago tuned basic list operators (flat, maps, map_filter);
2006-04-13 ago use conjunction stuff from conjunction.ML;
2006-03-08 ago tuned;
2006-03-05 ago SELECT_GOAL: fixed trivial case;
2006-03-04 ago added extract, retrofit;
2006-01-14 ago sane ERROR handling;
2005-12-23 ago Thm.compose_no_flatten;
2005-12-22 ago conclude/SELECT: Thm.bicompose_no_flatten avoids unsolicited modification of result;
2005-11-25 ago tuned names;
2005-11-19 ago tuned norm_hhf_protected;
2005-11-16 ago norm_hhf: no normalization of protected props;
2005-11-10 ago renamed Thm.cgoal_of to Thm.cprem_of;
2005-11-09 ago tuned;
2005-11-08 ago export compose_hhf;
2005-10-28 ago renamed Goal constant to prop, more general protect/unprotect interfaces;
2005-10-25 ago prove_raw: cterms, explicit asms;
2005-10-21 ago tuned;
2005-10-21 ago Internal goals.