src/HOL/Import/hol4rews.ML
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-10-23 wenzelm 2008-10-23 Thm.def_name;
2008-05-17 wenzelm 2008-05-17 structure Display: less pervasive operations;
2008-03-29 wenzelm 2008-03-29 simplified PureThy.store_thm;
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-04-04 wenzelm 2007-04-04 removed obsolete sign_of/sign_of_thm;
2006-12-15 wenzelm 2006-12-15 avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-11-27 haftmann 2006-11-27 removed HOL structure
2006-10-20 haftmann 2006-10-20 Symtab.foldl replaced by Symtab.fold
2006-10-09 wenzelm 2006-10-09 attribute: Context.mapping;
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list);
2006-02-03 wenzelm 2006-02-03 canonical member/insert/merge;
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2005-12-06 haftmann 2005-12-06 re-oriented some result tuples in PureThy
2005-09-26 obua 2005-09-26 fixed disambiguation problem
2005-09-23 obua 2005-09-23 1) fixed bug in type_introduction: first stage uses different namespace than second stage 2) fixed bug in dump_import_thy via gen2replay function
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-12 obua 2005-09-12 Added HOLLight support to importer.
2005-09-05 wenzelm 2005-09-05 curried_lookup/update;
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun;
2005-04-01 skalberg 2005-04-01 Updated import configuration.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-06-20 wenzelm 2004-06-20 got rid of Output.output for default print mode;
2004-05-29 wenzelm 2004-05-29 Output.output;
2004-04-17 skalberg 2004-04-17 Minor cleanup of headers and some speedup of the HOL4 import.
2004-04-04 skalberg 2004-04-04 Added a number of explicit type casts and delayed evaluations (all seemingly needless) so that SML/NJ 110.9.1 would accept the importer...
2004-04-02 skalberg 2004-04-02 Added HOL proof importer.