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;
wenzelm [Fri, 28 Oct 2005 22:27:52 +0200] rev 18025
added incr_indexes;
added lift_all (approx. reverse of gen_all);
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm [Fri, 28 Oct 2005 22:27:51 +0200] rev 18024
renamed Goal constant to prop;
wenzelm [Fri, 28 Oct 2005 22:27:47 +0200] rev 18023
accomodate simplified Thm.lift_rule;