2014-09-08 blanchet 2014-09-08 added flag to 'typedef' to allow concealed definitions
2014-04-03 blanchet 2014-04-03 use same idiom as used for datatype 'size' function to name constants and theorems emerging from various type interpretations -- reduces the chances of name clashes on theory merges
2013-12-31 wenzelm 2013-12-31 proper context for norm_hhf and derived operations; clarified tool context in some boundary cases;
2012-10-12 wenzelm 2012-10-12 discontinued typedef with alternative name;
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-10-12 wenzelm 2012-10-12 discontinued typedef with implicit set_def;
2012-04-23 wenzelm 2012-04-23 typedef with implicit set definition is considered legacy;
2012-03-31 wenzelm 2012-03-31 more direct Local_Defs.contract; eliminated slightly odd Local_Defs.trans_term/trans_prop;
2012-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-03-15 wenzelm 2012-03-15 prefer formally checked @{keyword} parser;
2012-03-15 wenzelm 2012-03-15 declare minor keywords via theory header;
2011-11-08 wenzelm 2011-11-08 more specific treatment of defines/assumes -- avoid normalizing defs by themselves (NB: locale specifications and Local_Theory.define may lead to arbitrary mixture);
2011-10-28 wenzelm 2011-10-28 uniform Local_Theory.declaration with explicit params;
2011-04-17 wenzelm 2011-04-17 added Binding.print convenience, which includes quote already;
2011-04-17 wenzelm 2011-04-17 report Name_Space.declare/define, relatively to context; added "global" variants of context-dependent declarations;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Lexicon;
2010-08-26 wenzelm 2010-08-26 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 haftmann 2010-08-12 Named_Target.theory_init
2010-08-11 haftmann 2010-08-11 renamed Theory_Target to the more appropriate Named_Target
2010-05-17 wenzelm 2010-05-17 prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-25 wenzelm 2010-04-25 modernized naming conventions of main Isar proof elements;
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 =; simplified via ProofContext.check_tfree;
2010-04-11 wenzelm 2010-04-11 expose foundational typedef axiom name;
2010-04-11 wenzelm 2010-04-11 Thm.add_axiom/add_def: return internal name of foundational axiom;
2010-03-27 wenzelm 2010-03-27 separate global and local part, only the latter is transformed by morphisms;
2010-03-19 wenzelm 2010-03-19 allow sort constraints in HOL/typedef and related HOLCF variants;
2010-03-18 wenzelm 2010-03-18 eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints;
2010-03-13 wenzelm 2010-03-13 Local_Theory.define handles hidden polymorphism;
2010-03-13 wenzelm 2010-03-13 localized typedef; Typedef.get_info can yield multiple typedef interpretations, even in a global context; misc tuning and modernization;
2010-03-09 wenzelm 2010-03-09 Typedecl.typedecl_global;
2010-03-07 wenzelm 2010-03-07 separate structure Typedecl;
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-03-03 wenzelm 2010-03-03 adapted to authentic syntax -- actual types are verbatim;
2010-02-24 wenzelm 2010-02-24 allow general mixfix syntax for type constructors;
2010-02-19 wenzelm 2010-02-19 Thm.def_binding;
2010-02-18 wenzelm 2010-02-18 typedef: slightly more precise treatment of binding; tuned;
2010-02-15 wenzelm 2010-02-15 Typedef.the_info;
2010-02-15 wenzelm 2010-02-15 discontinued unnamed infix syntax;
2010-02-07 wenzelm 2010-02-07 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-11-02 wenzelm 2009-11-02 modernized structure Primitive_Defs;
2009-11-01 wenzelm 2009-11-01 modernized structure Rule_Cases;
2009-10-29 wenzelm 2009-10-29 modernized functor/structures Interpretation;
2009-10-17 wenzelm 2009-10-17 operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
2009-10-17 wenzelm 2009-10-17 indicate CRITICAL nature of various setmp combinators;
2009-06-21 haftmann 2009-06-21 tuned interface
2009-06-19 haftmann 2009-06-19 discontinued ancient tradition to suffix certain ML module names with "_package"