huffman [Thu, 19 Jun 2008 22:50:58 +0200] rev 27289
move lemmas into locales;
restructure some proofs
huffman [Thu, 19 Jun 2008 22:43:59 +0200] rev 27288
add lemmas take_chain_less and take_chain_le
wenzelm [Thu, 19 Jun 2008 22:27:10 +0200] rev 27287
disposed Sign.read_typ etc;
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;