wenzelm [Thu, 18 Aug 2005 11:17:45 +0200] rev 17110
moved before proof.ML;
added FINDGOAL/HEADGOAL (from proof.ML);
added type method (from proof.ML);
moved proof refinement etc. to proof.ML;
tuned;
wenzelm [Thu, 18 Aug 2005 11:17:44 +0200] rev 17109
added add_locale_context(_i), which returns the body context for presentation;
note_thmss(_i), add_thmss: returns context for presentation;
removed map_attrib_specs/facts (cf. Attrib.map_specs/facts);
wenzelm [Thu, 18 Aug 2005 11:17:43 +0200] rev 17108
moved translation functions to Pure/sign.ML;
moved attribute preparation to actual operations in proof.ML etc.;
removed various trivial interfaces;
wenzelm [Thu, 18 Aug 2005 11:17:42 +0200] rev 17107
various Toplevel.theory_context commands: proper presentation in context;
simplified interfaces Proof vs. IsarThy;