src/HOL/Tools/typedef.ML
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"