| Sat, 14 Jan 2006 17:14:06 +0100 |
sane ERROR handling;
|
file | diff | annotate |
| Thu, 22 Dec 2005 12:27:10 +0100 |
Fixed a use of an outdated Substring function
|
file | diff | annotate |
| Tue, 06 Dec 2005 09:04:09 +0100 |
re-oriented some result tuples in PureThy
|
file | diff | annotate |
| Fri, 21 Oct 2005 18:14:38 +0200 |
OldGoals;
|
file | diff | annotate |
| Wed, 19 Oct 2005 21:52:29 +0200 |
replaced commafy by existing commas;
|
file | diff | annotate |
| Tue, 18 Oct 2005 17:59:27 +0200 |
Simplifier.theory_context;
|
file | diff | annotate |
| Mon, 26 Sep 2005 19:19:14 +0200 |
moved disambiguate_frees to ProofKernel;
|
file | diff | annotate |
| Mon, 26 Sep 2005 16:10:19 +0200 |
Release HOL4 and HOLLight Importer.
|
file | diff | annotate |
| Mon, 26 Sep 2005 02:27:14 +0200 |
fixed disambiguation problem
|
file | diff | annotate |
| Sat, 24 Sep 2005 23:55:17 +0200 |
set show_types and show_sorts during import
|
file | diff | annotate |
| Sat, 24 Sep 2005 13:26:40 +0200 |
remove debug clutter
|
file | diff | annotate |
| Sat, 24 Sep 2005 10:47:22 +0200 |
bug fix
|
file | diff | annotate |
| Fri, 23 Sep 2005 22:49:25 +0200 |
fix
|
file | diff | annotate |
| Fri, 23 Sep 2005 20:13:54 +0200 |
1) fixed bug in type_introduction: first stage uses different namespace than second stage
|
file | diff | annotate |
| Fri, 23 Sep 2005 10:01:14 +0200 |
replay type_introduction fix
|
file | diff | annotate |
| Fri, 23 Sep 2005 00:52:13 +0200 |
add debug messages
|
file | diff | annotate |
| Mon, 19 Sep 2005 22:35:39 +0200 |
maybe the last bug fix (sigh)?
|
file | diff | annotate |
| Sat, 17 Sep 2005 11:49:29 +0200 |
1) mapped .. and == constants
|
file | diff | annotate |
| Fri, 16 Sep 2005 21:02:15 +0200 |
fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
|
file | diff | annotate |
| Thu, 15 Sep 2005 17:16:56 +0200 |
TableFun/Symtab: curried lookup and update;
|
file | diff | annotate |
| Wed, 14 Sep 2005 19:03:16 +0200 |
Fixed Importer bug in type_introduction: instantiate type variables in rep-abs theorems exactly as it is done in HOL-light.
|
file | diff | annotate |
| Tue, 13 Sep 2005 17:05:59 +0200 |
fixed INST: has same semantic now as INST_TYPE for repetitions
|
file | diff | annotate |
| Mon, 12 Sep 2005 22:07:07 +0200 |
removed clutter
|
file | diff | annotate |
| Mon, 12 Sep 2005 17:29:07 +0200 |
introduced internal function hthm2thm
|
file | diff | annotate |
| Mon, 12 Sep 2005 15:52:00 +0200 |
Added HOLLight support to importer.
|
file | diff | annotate |
| Mon, 20 Jun 2005 22:13:59 +0200 |
get_thm(s): Name;
|
file | diff | annotate |
| Fri, 17 Jun 2005 18:33:12 +0200 |
refer to HOL4_PROOFS setting;
|
file | diff | annotate |
| Sat, 11 Jun 2005 22:15:47 +0200 |
renamed Sign.intern_tycon to Sign.intern_type;
|
file | diff | annotate |
| Thu, 21 Apr 2005 18:57:18 +0200 |
Adapted to new interface of instantiation and unification / matching functions.
|
file | diff | annotate |
| Fri, 01 Apr 2005 18:59:17 +0200 |
Updated import configuration.
|
file | diff | annotate |
| Fri, 04 Mar 2005 15:07:34 +0100 |
Removed practically all references to Library.foldr.
|
file | diff | annotate |
| Thu, 03 Mar 2005 12:43:01 +0100 |
Move towards standard functions.
|
file | diff | annotate |
| Sun, 13 Feb 2005 17:15:14 +0100 |
Deleted Library.option type.
|
file | diff | annotate |
| Mon, 24 Jan 2005 18:16:57 +0100 |
Adapted to modified interface of PureThy.get_thm(s).
|
file | diff | annotate |
| Sun, 20 Jun 2004 09:30:12 +0200 |
got rid of Output.output for default print mode;
|
file | diff | annotate |
| Sat, 29 May 2004 14:57:39 +0200 |
Output.output;
|
file | diff | annotate |
| Thu, 29 Apr 2004 06:03:18 +0200 |
more robust output of definitions;
|
file | diff | annotate |
| Mon, 26 Apr 2004 14:54:45 +0200 |
use Syntax.is_identifier;
|
file | diff | annotate |
| Sat, 17 Apr 2004 23:53:35 +0200 |
Minor cleanup of headers and some speedup of the HOL4 import.
|
file | diff | annotate |
| Sun, 04 Apr 2004 15:34:14 +0200 |
Added a number of explicit type casts and delayed evaluations (all seemingly
|
file | diff | annotate |
| Fri, 02 Apr 2004 17:37:45 +0200 |
Added HOL proof importer.
|
file | diff | annotate |