wenzelm [Fri, 28 Oct 2005 22:28:07 +0200] rev 18037
syntax for literal facts;
wenzelm [Fri, 28 Oct 2005 22:28:06 +0200] rev 18036
removed try_dest_Goal, use Logic.unprotect;
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;