Thu, 19 Jun 2008 21:14:30 +0200tuned signature;
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);

Thu, 19 Jun 2008 20:48:06 +0200private add_used (from drule.ML);
wenzelm [Thu, 19 Jun 2008 20:48:06 +0200] rev 27282
private add_used (from drule.ML);
Variable.declare_names;

Thu, 19 Jun 2008 20:48:05 +0200Variable.declare_typ;
wenzelm [Thu, 19 Jun 2008 20:48:05 +0200] rev 27281
Variable.declare_typ;

Thu, 19 Jun 2008 20:48:04 +0200added declare_typ;
wenzelm [Thu, 19 Jun 2008 20:48:04 +0200] rev 27280
added declare_typ;

Thu, 19 Jun 2008 20:48:03 +0200moved add_used to Isar/rule_insts.ML;
wenzelm [Thu, 19 Jun 2008 20:48:03 +0200] rev 27279
moved add_used to Isar/rule_insts.ML;

Thu, 19 Jun 2008 20:48:02 +0200export read_typ/cert_typ -- version with regular context operations;
wenzelm [Thu, 19 Jun 2008 20:48:02 +0200] rev 27278
export read_typ/cert_typ -- version with regular context operations;
tuned;

Thu, 19 Jun 2008 20:48:01 +0200export read_typ/cert_typ -- version with regular context operations;
wenzelm [Thu, 19 Jun 2008 20:48:01 +0200] rev 27277
export read_typ/cert_typ -- version with regular context operations;

Thu, 19 Jun 2008 20:48:00 +0200tuned signature;
wenzelm [Thu, 19 Jun 2008 20:48:00 +0200] rev 27276
tuned signature;
removed duplicate of RecordPackage.read_typ;
replaced Typetab by existing Typtab;

Thu, 19 Jun 2008 20:47:58 +0200removed duplicate of DatatypePackage.read_typ;
wenzelm [Thu, 19 Jun 2008 20:47:58 +0200] rev 27275
removed duplicate of DatatypePackage.read_typ;

Thu, 19 Jun 2008 20:34:28 +0200add lemma cfcomp_LAM
huffman [Thu, 19 Jun 2008 20:34:28 +0200] rev 27274
add lemma cfcomp_LAM