src/HOL/Import/proof_kernel.ML
Fri, 16 Sep 2005 21:02:15 +0200 obua fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
Thu, 15 Sep 2005 17:16:56 +0200 wenzelm TableFun/Symtab: curried lookup and update;
Wed, 14 Sep 2005 19:03:16 +0200 obua Fixed Importer bug in type_introduction: instantiate type variables in rep-abs theorems exactly as it is done in HOL-light.
Tue, 13 Sep 2005 17:05:59 +0200 obua fixed INST: has same semantic now as INST_TYPE for repetitions
Mon, 12 Sep 2005 22:07:07 +0200 obua removed clutter
Mon, 12 Sep 2005 17:29:07 +0200 obua introduced internal function hthm2thm
Mon, 12 Sep 2005 15:52:00 +0200 obua Added HOLLight support to importer.
Mon, 20 Jun 2005 22:13:59 +0200 wenzelm get_thm(s): Name;
Fri, 17 Jun 2005 18:33:12 +0200 wenzelm refer to HOL4_PROOFS setting;
Sat, 11 Jun 2005 22:15:47 +0200 wenzelm renamed Sign.intern_tycon to Sign.intern_type;
Thu, 21 Apr 2005 18:57:18 +0200 berghofe Adapted to new interface of instantiation and unification / matching functions.
Fri, 01 Apr 2005 18:59:17 +0200 skalberg Updated import configuration.
Fri, 04 Mar 2005 15:07:34 +0100 skalberg Removed practically all references to Library.foldr.
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Mon, 24 Jan 2005 18:16:57 +0100 berghofe Adapted to modified interface of PureThy.get_thm(s).
Sun, 20 Jun 2004 09:30:12 +0200 wenzelm got rid of Output.output for default print mode;
Sat, 29 May 2004 14:57:39 +0200 wenzelm Output.output;
Thu, 29 Apr 2004 06:03:18 +0200 wenzelm more robust output of definitions;
Mon, 26 Apr 2004 14:54:45 +0200 wenzelm use Syntax.is_identifier;
Sat, 17 Apr 2004 23:53:35 +0200 skalberg Minor cleanup of headers and some speedup of the HOL4 import.
Sun, 04 Apr 2004 15:34:14 +0200 skalberg Added a number of explicit type casts and delayed evaluations (all seemingly
Fri, 02 Apr 2004 17:37:45 +0200 skalberg Added HOL proof importer.
less more (0) tip