2010-04-28 ago tuned user-level type abbrevs: explicit warning concerning ignored sort constraints -- sorts never affect formation of types and type abbrevs strip sorts internally;
2010-04-16 ago replaced old Sign.add_tyabbrs(_i) by Sign.add_type_abbrev (without mixfix);
2010-04-16 ago allow syntax types within abbreviations;
2010-04-16 ago local type abbreviations;
2010-04-15 ago explicit ProofContext.check_tfree;
2010-04-15 ago replaced slightly odd Typedecl.predeclare_constraints by plain declaration of type arguments -- also avoid "recursive" declaration of type constructor, which can cause problems with sequential definitions =;
2010-03-19 ago support type arguments with sort constraints;
2010-03-18 ago eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
2010-03-13 ago added typedecl_wrt, which affects default sorts of type args;
2010-03-11 ago actually apply morphism to binding;
2010-03-09 ago localized typedecl;
2010-03-07 ago separate structure Typedecl;