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;
Thu, 18 Aug 2005 11:17:37 +0200 added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm [Thu, 18 Aug 2005 11:17:37 +0200] rev 17102
added interfaces for compile translation functions (from Isar/isar_thy.ML);
Thu, 18 Aug 2005 11:17:36 +0200 added tap;
wenzelm [Thu, 18 Aug 2005 11:17:36 +0200] rev 17101
added tap;
Thu, 18 Aug 2005 11:17:35 +0200 updated;
wenzelm [Thu, 18 Aug 2005 11:17:35 +0200] rev 17100
updated;
Thu, 18 Aug 2005 11:17:34 +0200 usedir: tuned option -V;
wenzelm [Thu, 18 Aug 2005 11:17:34 +0200] rev 17099
usedir: tuned option -V;
Thu, 18 Aug 2005 11:17:33 +0200 usedir: removed option -H;
wenzelm [Thu, 18 Aug 2005 11:17:33 +0200] rev 17098
usedir: removed option -H;
Thu, 18 Aug 2005 11:17:32 +0200 * Proper output of proof terms within a proof context;
wenzelm [Thu, 18 Aug 2005 11:17:32 +0200] rev 17097
* Proper output of proof terms within a proof context; * Proper output of antiquotations for theory commands involving a proof context; * 'print_theorems': in theory mode print difference of facts, in proof mode print local facts;
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip