Thu, 18 Aug 2005 11:17:47 +0200 moved after method.ML;
wenzelm [Thu, 18 Aug 2005 11:17:47 +0200] rev 17112
moved after method.ML; moved FINDGOAL/HEADGOAL to method.ML; moved type method to method.ML; prepare attributes here; tuned various interfaces (cf. isar_thy.ML); tuned;
Thu, 18 Aug 2005 11:17:46 +0200 prepare attributes here;
wenzelm [Thu, 18 Aug 2005 11:17:46 +0200] rev 17111
prepare attributes here; tuned;
Thu, 18 Aug 2005 11:17:45 +0200 moved before proof.ML;
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;
Thu, 18 Aug 2005 11:17:44 +0200 added add_locale_context(_i), which returns the body context for presentation;
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);
Thu, 18 Aug 2005 11:17:43 +0200 moved translation functions to Pure/sign.ML;
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;
Thu, 18 Aug 2005 11:17:42 +0200 various Toplevel.theory_context commands: proper presentation in context;
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;
Thu, 18 Aug 2005 11:17:41 +0200 use theory instead of obsolete Sign.sg;
wenzelm [Thu, 18 Aug 2005 11:17:41 +0200] rev 17106
use theory instead of obsolete Sign.sg; tuned comments;
Thu, 18 Aug 2005 11:17:40 +0200 added map_specs/facts operators (from locale.ML);
wenzelm [Thu, 18 Aug 2005 11:17:40 +0200] rev 17105
added map_specs/facts operators (from locale.ML);
Thu, 18 Aug 2005 11:17:39 +0200 removed obsolete Theory.sign_of;
wenzelm [Thu, 18 Aug 2005 11:17:39 +0200] rev 17104
removed obsolete Theory.sign_of;
Thu, 18 Aug 2005 11:17:38 +0200 load method.ML before proof.ML;
wenzelm [Thu, 18 Aug 2005 11:17:38 +0200] rev 17103
load method.ML before proof.ML;
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip