src/HOL/Import/proof_kernel.ML
2007-04-15 wenzelm 2007-04-15 removed obsolete TypeInfer.logicT -- use dummyT;
2007-04-15 wenzelm 2007-04-15 Thm.fold_terms;
2007-04-14 wenzelm 2007-04-14 cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
2007-04-04 wenzelm 2007-04-04 rep_thm/cterm/ctyp: removed obsolete sign field;
2006-10-04 haftmann 2006-10-04 insert replacing ins ins_int ins_string
2006-09-06 haftmann 2006-09-06 TypedefPackage.add_typedef_* now yields name of introduced type constructor
2006-08-02 wenzelm 2006-08-02 removed obsolete Drule.frees/vars_of etc.;
2006-07-04 wenzelm 2006-07-04 Thm.varifyT;
2006-06-13 wenzelm 2006-06-13 use Drule.unvarify instead of obsolete Drule.freeze_all;
2006-05-20 wenzelm 2006-05-20 List.partition;
2006-04-06 haftmann 2006-04-06 cleanup in typedef/datatype package
2006-03-14 wenzelm 2006-03-14 string_of_mixfix;
2006-02-16 obua 2006-02-16 cache improvements
2006-02-16 obua 2006-02-16 variable counter is now also cached
2006-02-16 obua 2006-02-16 adapted to kernel changes
2006-02-15 obua 2006-02-15 fixed bugs, added caching
2006-02-06 wenzelm 2006-02-06 Envir.(beta_)eta_contract;
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-14 wenzelm 2006-01-14 sane ERROR handling;
2005-12-22 paulson 2005-12-22 Fixed a use of an outdated Substring function
2005-12-06 haftmann 2005-12-06 re-oriented some result tuples in PureThy
2005-10-21 wenzelm 2005-10-21 OldGoals;
2005-10-19 wenzelm 2005-10-19 replaced commafy by existing commas; avoid obsolete Goals.prin;
2005-10-18 wenzelm 2005-10-18 Simplifier.theory_context; replaced get_const by Sign.the_const_type; eliminated obsolete sign_of;
2005-09-26 wenzelm 2005-09-26 moved disambiguate_frees to ProofKernel;
2005-09-26 obua 2005-09-26 Release HOL4 and HOLLight Importer.
2005-09-26 obua 2005-09-26 fixed disambiguation problem
2005-09-24 obua 2005-09-24 set show_types and show_sorts during import
2005-09-24 obua 2005-09-24 remove debug clutter
2005-09-24 obua 2005-09-24 bug fix
2005-09-23 obua 2005-09-23 fix
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-23 obua 2005-09-23 replay type_introduction fix
2005-09-23 obua 2005-09-23 add debug messages
2005-09-19 obua 2005-09-19 maybe the last bug fix (sigh)?
2005-09-17 obua 2005-09-17 1) mapped .. and == constants 2) improved protect_varname
2005-09-16 obua 2005-09-16 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-14 obua 2005-09-14 Fixed Importer bug in type_introduction: instantiate type variables in rep-abs theorems exactly as it is done in HOL-light.
2005-09-13 obua 2005-09-13 fixed INST: has same semantic now as INST_TYPE for repetitions
2005-09-12 obua 2005-09-12 removed clutter
2005-09-12 obua 2005-09-12 introduced internal function hthm2thm
2005-09-12 obua 2005-09-12 Added HOLLight support to importer.
2005-06-20 wenzelm 2005-06-20 get_thm(s): Name;
2005-06-17 wenzelm 2005-06-17 refer to HOL4_PROOFS setting; accomodate identification of type Sign.sg and theory;
2005-06-11 wenzelm 2005-06-11 renamed Sign.intern_tycon to Sign.intern_type;
2005-04-21 berghofe 2005-04-21 Adapted to new interface of instantiation and unification / matching functions.
2005-04-01 skalberg 2005-04-01 Updated import configuration.
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-01-24 berghofe 2005-01-24 Adapted to modified interface of PureThy.get_thm(s).
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-29 wenzelm 2004-04-29 more robust output of definitions;
2004-04-26 wenzelm 2004-04-26 use Syntax.is_identifier;
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.