src/HOL/Tools/typecopy.ML
2010-03-27 wenzelm 2010-03-27 Typedef.info: separate global and local part, only the latter is transformed by morphisms;
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-19 wenzelm 2010-03-19 typedef etc.: no constraints;
2010-03-13 wenzelm 2010-03-13 adapted to localized typedef: handle single global interpretation only;
2009-11-10 wenzelm 2009-11-10 modernized structure Theory_Target;
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-10-29 wenzelm 2009-10-29 modernized functor/structures Interpretation;
2009-08-15 haftmann 2009-08-15 tuned
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"