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;
wenzelm [Thu, 19 Jun 2008 20:48:00 +0200] rev 27276
tuned signature;
removed duplicate of RecordPackage.read_typ;
replaced Typetab by existing Typtab;
wenzelm [Thu, 19 Jun 2008 20:47:58 +0200] rev 27275
removed duplicate of DatatypePackage.read_typ;
huffman [Thu, 19 Jun 2008 20:34:28 +0200] rev 27274
add lemma cfcomp_LAM
wenzelm [Thu, 19 Jun 2008 17:32:18 +0200] rev 27273
add_abbrev: check tfrees of rhs, not tvars (addresses a lapse introduced in 1.65);
urbanc [Thu, 19 Jun 2008 15:47:26 +0200] rev 27272
slightly tuned
krauss [Thu, 19 Jun 2008 11:46:14 +0200] rev 27271
generalized induct_scheme method to prove conditional induction schemes.