wenzelm [Thu, 19 Jun 2008 22:05:05 +0200] rev 27286
renamed is_abbrev_mode to abbrev_mode;
added private get_sort (from sign.ML);
wenzelm [Thu, 19 Jun 2008 22:05:04 +0200] rev 27285
ProofContext.abbrev_mode;
wenzelm [Thu, 19 Jun 2008 22:05:01 +0200] rev 27284
moved get_sort to Isar/proof_context.ML;
removed obsolete read_def_typ, read_typ, read_typ_syntax, read_typ_abbrev;
wenzelm [Thu, 19 Jun 2008 21:14:30 +0200] rev 27283
tuned signature;
removed duplicates of read_typ/cert_typ (cf. RecordPackage.read_typ/cert_typ);
wenzelm [Thu, 19 Jun 2008 20:48:06 +0200] rev 27282
private add_used (from drule.ML);
Variable.declare_names;
wenzelm [Thu, 19 Jun 2008 20:48:05 +0200] rev 27281
Variable.declare_typ;
wenzelm [Thu, 19 Jun 2008 20:48:04 +0200] rev 27280
added declare_typ;
wenzelm [Thu, 19 Jun 2008 20:48:03 +0200] rev 27279
moved add_used to Isar/rule_insts.ML;
wenzelm [Thu, 19 Jun 2008 20:48:02 +0200] rev 27278
export read_typ/cert_typ -- version with regular context operations;
tuned;
wenzelm [Thu, 19 Jun 2008 20:48:01 +0200] rev 27277
export read_typ/cert_typ -- version with regular context operations;