src/Pure/Isar/typedecl.ML
2010-04-28 wenzelm 2010-04-28 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 wenzelm 2010-04-16 replaced old Sign.add_tyabbrs(_i) by Sign.add_type_abbrev (without mixfix); misc tuning and simplification;
2010-04-16 wenzelm 2010-04-16 allow syntax types within abbreviations;
2010-04-16 wenzelm 2010-04-16 local type abbreviations;
2010-04-15 wenzelm 2010-04-15 explicit ProofContext.check_tfree;
2010-04-15 wenzelm 2010-04-15 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 B.foo = A.foo; simplified via ProofContext.check_tfree;
2010-03-19 wenzelm 2010-03-19 support type arguments with sort constraints;
2010-03-18 wenzelm 2010-03-18 eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types); allow sort constraints; misc tuning and clarification;
2010-03-13 wenzelm 2010-03-13 added typedecl_wrt, which affects default sorts of type args; misc tuning and simplification;
2010-03-11 wenzelm 2010-03-11 actually apply morphism to binding;
2010-03-09 wenzelm 2010-03-09 localized typedecl;
2010-03-07 wenzelm 2010-03-07 separate structure Typedecl;