Thu, 27 Jul 2006 13:43:12 +0200 added legacy_pretty_thm (with fall-back on ProtoPure.thy);
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;
Thu, 27 Jul 2006 13:43:11 +0200 Assumption.assume;
wenzelm [Thu, 27 Jul 2006 13:43:11 +0200] rev 20233
Assumption.assume; moved Goal.norm_hhf(_protect) to meta_simplifier.ML (pervasive);
Thu, 27 Jul 2006 13:43:10 +0200 removed obsolete is_fact (cf. Thm.no_prems);
wenzelm [Thu, 27 Jul 2006 13:43:10 +0200] rev 20232
removed obsolete is_fact (cf. Thm.no_prems);
Thu, 27 Jul 2006 13:43:09 +0200 tuned interfaces;
wenzelm [Thu, 27 Jul 2006 13:43:09 +0200] rev 20231
tuned interfaces; moved basic assumption operations from structure ProofContext to Assumption;
Thu, 27 Jul 2006 13:43:08 +0200 read_def_cterms (legacy version): Consts.certify;
wenzelm [Thu, 27 Jul 2006 13:43:08 +0200] rev 20230
read_def_cterms (legacy version): Consts.certify;
Thu, 27 Jul 2006 13:43:07 +0200 Assumption.assume;
wenzelm [Thu, 27 Jul 2006 13:43:07 +0200] rev 20229
Assumption.assume;
Thu, 27 Jul 2006 13:43:06 +0200 moved Goal.norm_hhf(_protect) to meta_simplifier.ML (pervasive);
wenzelm [Thu, 27 Jul 2006 13:43:06 +0200] rev 20228
moved Goal.norm_hhf(_protect) to meta_simplifier.ML (pervasive);
Thu, 27 Jul 2006 13:43:05 +0200 removed obsolete equal_abs_elim(_list);
wenzelm [Thu, 27 Jul 2006 13:43:05 +0200] rev 20227
removed obsolete equal_abs_elim(_list);
Thu, 27 Jul 2006 13:43:04 +0200 removed obsolete pretty_thm_no_quote;
wenzelm [Thu, 27 Jul 2006 13:43:04 +0200] rev 20226
removed obsolete pretty_thm_no_quote;
Thu, 27 Jul 2006 13:43:03 +0200 added Pure/assumption.ML;
wenzelm [Thu, 27 Jul 2006 13:43:03 +0200] rev 20225
added Pure/assumption.ML;
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip