src/Pure/goal.ML
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.