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