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