src/Pure/Isar/typedecl.ML
2011-04-17 ago added Binding.print convenience, which includes quote already;
2011-04-17 ago report Name_Space.declare/define, relatively to context;
2011-04-16 ago modernized structure Proof_Context;
2010-08-27 ago more careful treatment of context visibility flag wrt. spurious warnings;
2010-08-26 ago renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
2010-08-12 ago Named_Target.theory_init
2010-08-11 ago renamed Theory_Target to the more appropriate Named_Target
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 B.foo = A.foo;
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;