wenzelm [Fri, 28 Oct 2005 22:28:04 +0200] rev 18035
added cgoal_of;
simplified lift_rule: take goal cterm instead of goal state thm, use Logic.lift_abs/all;
wenzelm [Fri, 28 Oct 2005 22:28:03 +0200] rev 18034
accomodate simplified Thm.lift_rule;
tuned;
wenzelm [Fri, 28 Oct 2005 22:28:02 +0200] rev 18033
export cong_modifiers, simp_modifiers';
wenzelm [Fri, 28 Oct 2005 22:28:00 +0200] rev 18032
certify_term: tuned monomorphic consts;
wenzelm [Fri, 28 Oct 2005 22:27:59 +0200] rev 18031
datatype thmref: added Fact;
renamed Goal constant to prop;
wenzelm [Fri, 28 Oct 2005 22:27:58 +0200] rev 18030
Logic.lift_all;
wenzelm [Fri, 28 Oct 2005 22:27:57 +0200] rev 18029
renamed Goal constant to prop, more general protect/unprotect interfaces;
replaced lift_fns by lift_abs, lift_all;
wenzelm [Fri, 28 Oct 2005 22:27:56 +0200] rev 18028
renamed Goal.norm_hhf_rule to Goal.norm_hhf;
wenzelm [Fri, 28 Oct 2005 22:27:55 +0200] rev 18027
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;
wenzelm [Fri, 28 Oct 2005 22:27:54 +0200] rev 18026
added add_local/add_global;
index props (for add_local only);
added could_unify;