Wed, 18 Jun 2008 23:07:30 +0200 replace preorder class with locale
huffman [Wed, 18 Jun 2008 23:07:30 +0200] rev 27268
replace preorder class with locale
Wed, 18 Jun 2008 23:03:11 +0200 add lemma compact_imp_principal to locale ideal_completion
huffman [Wed, 18 Jun 2008 23:03:11 +0200] rev 27267
add lemma compact_imp_principal to locale ideal_completion
Wed, 18 Jun 2008 22:32:06 +0200 added type_constraint (formerly in type_infer.ML, which is now loaded later);
wenzelm [Wed, 18 Jun 2008 22:32:06 +0200] rev 27266
added type_constraint (formerly in type_infer.ML, which is now loaded later);
Wed, 18 Jun 2008 22:32:04 +0200 TypeExt.type_constraint;
wenzelm [Wed, 18 Jun 2008 22:32:04 +0200] rev 27265
TypeExt.type_constraint;
Wed, 18 Jun 2008 22:32:03 +0200 simplified TypeInfer.infer_types;
wenzelm [Wed, 18 Jun 2008 22:32:03 +0200] rev 27264
simplified TypeInfer.infer_types;
Wed, 18 Jun 2008 22:32:02 +0200 improved error output -- variant/mark bounds;
wenzelm [Wed, 18 Jun 2008 22:32:02 +0200] rev 27263
improved error output -- variant/mark bounds; simplified infer_types -- always freeze, no result substitution;
(0) -10000 -3000 -1000 -300 -100 -30 -10 -6 +6 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip