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.
huffman [Thu, 19 Jun 2008 00:02:08 +0200] rev 27270
add lemma iterate_iterate
wenzelm [Wed, 18 Jun 2008 23:15:41 +0200] rev 27269
* Disposed old term read functions;
huffman [Wed, 18 Jun 2008 23:07:30 +0200] rev 27268
replace preorder class with locale
huffman [Wed, 18 Jun 2008 23:03:11 +0200] rev 27267
add lemma compact_imp_principal to locale ideal_completion
wenzelm [Wed, 18 Jun 2008 22:32:06 +0200] rev 27266
added type_constraint (formerly in type_infer.ML, which is now loaded later);
wenzelm [Wed, 18 Jun 2008 22:32:04 +0200] rev 27265
TypeExt.type_constraint;
wenzelm [Wed, 18 Jun 2008 22:32:03 +0200] rev 27264
simplified TypeInfer.infer_types;