src/HOL/Tools/typedef.ML
2015-09-24 wenzelm 2015-09-24 more explicit Defs.context: use proper name spaces as far as possible;
2015-09-24 wenzelm 2015-09-24 explicit indication of overloaded typedefs;
2015-09-23 wenzelm 2015-09-23 tuned signature;
2015-09-22 wenzelm 2015-09-22 eliminated separate type Theory.dep: use typeargs uniformly for consts/types; Object_Logic.add_judgment more like Theory.specify_const;
2015-09-22 wenzelm 2015-09-22 tuned signature;
2015-09-22 wenzelm 2015-09-22 tuned whitespace;
2015-09-22 wenzelm 2015-09-22 HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015; defs.ML: track dependencies also for type constructors; typedef.ML: add type defined by typedef to dependencies, Abs and Rep now depend on the type; Pure types and typedecls are final -- no dependencies;
2015-09-03 wenzelm 2015-09-03 more general Typedef.bindings; tuned signature;
2015-09-03 wenzelm 2015-09-03 trim context for persistent storage;
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
2015-03-31 wenzelm 2015-03-31 clarified role of naming for background theory: transform_binding (e.g. for "concealed" flag) uses naming of hypothetical context;
2015-03-31 wenzelm 2015-03-31 tuned signature;
2014-11-09 wenzelm 2014-11-09 proper proof context for typedef;
2014-10-13 wenzelm 2014-10-13 module Interpretation is superseded by Plugin;
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 B.foo = A.foo; 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 Typedef.info: 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;