src/HOLCF/Tools/pcpodef.ML
2010-03-27 wenzelm 2010-03-27 Typedef.info: separate global and local part, only the latter is transformed by morphisms;
2010-03-22 huffman 2010-03-22 error -> raise Fail
2010-03-22 huffman 2010-03-22 fix ML warnings in pcpodef.ML
2010-03-19 wenzelm 2010-03-19 allow sort constraints in HOL/typedef and related HOLCF variants;
2010-03-13 wenzelm 2010-03-13 global typedef;
2010-02-24 wenzelm 2010-02-24 allow general mixfix syntax for type constructors;
2010-02-18 wenzelm 2010-02-18 Sign.restore_naming -- slightly more robust;
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-13 huffman 2009-11-13 merged
2009-11-13 huffman 2009-11-13 cleaned up, removed unneeded call to Syntax.check_term
2009-11-13 wenzelm 2009-11-13 modernized structure Local_Theory;
2009-11-12 huffman 2009-11-12 improved ML interface to pcpodef
2009-11-11 huffman 2009-11-11 use Drule.standard (following typedef package), add pcpodef tactic interface
2009-11-10 wenzelm 2009-11-10 modernized structure Theory_Target;
2009-10-27 wenzelm 2009-10-27 comment;
2009-06-21 haftmann 2009-06-21 discontinued ancient tradition to suffix certain ML module names with "_package"