wenzelm [Thu, 27 Jul 2006 15:33:21 +0200] rev 20238
eliminated obsolete freeze_thaw;
webertj [Thu, 27 Jul 2006 14:21:57 +0200] rev 20237
type annotation added to make SML/NJ happy
wenzelm [Thu, 27 Jul 2006 13:44:03 +0200] rev 20236
"moved basic assumption operations from structure ProofContext to Assumption;"
wenzelm [Thu, 27 Jul 2006 13:43:13 +0200] rev 20235
ProofContext.legacy_pretty_thm;
wenzelm [Thu, 27 Jul 2006 13:43:12 +0200] rev 20234
added legacy_pretty_thm (with fall-back on ProtoPure.thy);
moved basic assumption operations to assumption.ML;
tuned;
wenzelm [Thu, 27 Jul 2006 13:43:11 +0200] rev 20233
Assumption.assume;
moved Goal.norm_hhf(_protect) to meta_simplifier.ML (pervasive);
wenzelm [Thu, 27 Jul 2006 13:43:10 +0200] rev 20232
removed obsolete is_fact (cf. Thm.no_prems);
wenzelm [Thu, 27 Jul 2006 13:43:09 +0200] rev 20231
tuned interfaces;
moved basic assumption operations from structure ProofContext to Assumption;
wenzelm [Thu, 27 Jul 2006 13:43:08 +0200] rev 20230
read_def_cterms (legacy version): Consts.certify;
wenzelm [Thu, 27 Jul 2006 13:43:07 +0200] rev 20229
Assumption.assume;