| Wed, 25 Jun 2008 17:38:32 +0200 |
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
|
file | diff | annotate |
| Thu, 12 Jun 2008 23:12:54 +0200 |
use regular error function;
|
file | diff | annotate |
| Sun, 18 May 2008 15:04:09 +0200 |
moved global pretty/string_of functions from Sign to Syntax;
|
file | diff | annotate |
| Sat, 17 May 2008 13:54:30 +0200 |
structure Display: less pervasive operations;
|
file | diff | annotate |
| Sat, 12 Apr 2008 17:00:35 +0200 |
rep_cterm/rep_thm: no longer dereference theory_ref;
|
file | diff | annotate |
| Thu, 20 Mar 2008 00:20:44 +0100 |
simplified get_thm(s): back to plain name argument;
|
file | diff | annotate |
| Wed, 19 Mar 2008 22:27:57 +0100 |
renamed datatype thmref to Facts.ref, tuned interfaces;
|
file | diff | annotate |
| Thu, 11 Oct 2007 19:10:17 +0200 |
moved Drule.unvarify to Thm.unvarify (cf. more_thm.ML);
|
file | diff | annotate |
| Tue, 25 Sep 2007 17:06:14 +0200 |
proper Sign operations instead of Theory aliases;
|
file | diff | annotate |
| Tue, 25 Sep 2007 13:28:37 +0200 |
Syntax.parse/check/read;
|
file | diff | annotate |
| Tue, 18 Sep 2007 18:05:37 +0200 |
simplified PrintMode interfaces;
|
file | diff | annotate |
| Tue, 18 Sep 2007 16:08:00 +0200 |
simplified type int (eliminated IntInf.int, integer);
|
file | diff | annotate |
| Sun, 15 Apr 2007 23:25:50 +0200 |
removed obsolete TypeInfer.logicT -- use dummyT;
|
file | diff | annotate |
| Sun, 15 Apr 2007 14:31:47 +0200 |
Thm.fold_terms;
|
file | diff | annotate |
| Sat, 14 Apr 2007 17:35:52 +0200 |
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
|
file | diff | annotate |
| Wed, 04 Apr 2007 23:29:33 +0200 |
rep_thm/cterm/ctyp: removed obsolete sign field;
|
file | diff | annotate |
| Wed, 04 Oct 2006 14:17:38 +0200 |
insert replacing ins ins_int ins_string
|
file | diff | annotate |
| Wed, 06 Sep 2006 10:01:04 +0200 |
TypedefPackage.add_typedef_* now yields name of introduced type constructor
|
file | diff | annotate |
| Wed, 02 Aug 2006 22:26:37 +0200 |
removed obsolete Drule.frees/vars_of etc.;
|
file | diff | annotate |
| Tue, 04 Jul 2006 19:49:49 +0200 |
Thm.varifyT;
|
file | diff | annotate |
| Tue, 13 Jun 2006 23:41:31 +0200 |
use Drule.unvarify instead of obsolete Drule.freeze_all;
|
file | diff | annotate |
| Sat, 20 May 2006 23:36:55 +0200 |
List.partition;
|
file | diff | annotate |
| Thu, 06 Apr 2006 16:13:17 +0200 |
cleanup in typedef/datatype package
|
file | diff | annotate |
| Tue, 14 Mar 2006 22:06:31 +0100 |
string_of_mixfix;
|
file | diff | annotate |
| Thu, 16 Feb 2006 14:59:57 +0100 |
cache improvements
|
file | diff | annotate |
| Thu, 16 Feb 2006 04:17:19 +0100 |
variable counter is now also cached
|
file | diff | annotate |
| Thu, 16 Feb 2006 03:23:57 +0100 |
adapted to kernel changes
|
file | diff | annotate |
| Wed, 15 Feb 2006 23:57:06 +0100 |
fixed bugs, added caching
|
file | diff | annotate |
| Mon, 06 Feb 2006 20:58:54 +0100 |
Envir.(beta_)eta_contract;
|
file | diff | annotate |
| Sat, 21 Jan 2006 23:02:14 +0100 |
simplified type attribute;
|
file | diff | annotate |
| 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 |