src/HOL/Import/hol4rews.ML
2010-05-05 ago farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-02-21 ago proper markup of const syntax;
2010-02-07 ago renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2009-11-24 ago curried take/drop
2009-11-08 ago adapted Theory_Data;
2009-10-21 ago curried union as canonical list operation
2009-10-21 ago dropped redundant gen_ prefix
2009-10-17 ago eliminated hard tabulators, guessing at each author's individual tab-width;
2009-10-17 ago explicitly qualify Drule.standard;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-08-28 ago modernized messages -- eliminated ctyp/cterm operations;
2009-07-09 ago renamed functor TableFun to Table, and GraphFun to Graph;
2009-03-15 ago simplified attribute setup;
2009-03-08 ago moved basic algebra of long names from structure NameSpace to Long_Name;
2009-01-21 ago binding replaces bstring
2008-12-04 ago cleaned up binding module and related code
2008-10-23 ago Thm.def_name;
2008-05-17 ago structure Display: less pervasive operations;
2008-03-29 ago simplified PureThy.store_thm;
2007-05-07 ago simplified DataFun interfaces;
2007-04-04 ago removed obsolete sign_of/sign_of_thm;
2006-12-15 ago avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-11-27 ago removed HOL structure
2006-10-20 ago Symtab.foldl replaced by Symtab.fold
2006-10-09 ago attribute: Context.mapping;
2006-07-11 ago replaced Term.variant(list) by Name.variant(_list);
2006-02-03 ago canonical member/insert/merge;
2006-01-21 ago simplified type attribute;
2006-01-19 ago setup: theory -> theory;
2005-12-06 ago re-oriented some result tuples in PureThy
2005-09-26 ago fixed disambiguation problem
2005-09-23 ago 1) fixed bug in type_introduction: first stage uses different namespace than second stage
2005-09-15 ago TableFun/Symtab: curried lookup and update;
2005-09-12 ago Added HOLLight support to importer.
2005-09-05 ago curried_lookup/update;
2005-06-17 ago accomodate change of TheoryDataFun;
2005-04-01 ago Updated import configuration.
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2004-06-20 ago got rid of Output.output for default print mode;
2004-05-29 ago Output.output;
2004-04-17 ago Minor cleanup of headers and some speedup of the HOL4 import.
2004-04-04 ago Added a number of explicit type casts and delayed evaluations (all seemingly
2004-04-02 ago Added HOL proof importer.