Mon, 18 Sep 2000 14:10:31 +0200 |
wenzelm |
indicate occurrences of 'handle _';
|
file |
diff |
annotate
|
Thu, 07 Sep 2000 20:59:37 +0200 |
wenzelm |
use Rulify.rulify_no_asm;
|
file |
diff |
annotate
|
Tue, 05 Sep 2000 18:53:21 +0200 |
wenzelm |
proper handling of hints;
|
file |
diff |
annotate
|
Wed, 30 Aug 2000 10:21:19 +0200 |
nipkow |
Fixed rulify.
|
file |
diff |
annotate
|
Fri, 18 Aug 2000 17:58:33 +0200 |
wenzelm |
proper handling of defs;
|
file |
diff |
annotate
|
Thu, 17 Aug 2000 18:31:12 +0200 |
nipkow |
installed recdef congs data
|
file |
diff |
annotate
|
Tue, 25 Jul 2000 17:47:55 +0200 |
nipkow |
Replaced force by fast because force may now take forever to fail
|
file |
diff |
annotate
|
Fri, 05 May 2000 22:34:40 +0200 |
wenzelm |
tuned messages;
|
file |
diff |
annotate
|
Fri, 14 Apr 2000 01:14:51 +0200 |
wenzelm |
use HOLogic.termT;
|
file |
diff |
annotate
|
Fri, 31 Mar 2000 10:23:15 +0200 |
nipkow |
comments modified
|
file |
diff |
annotate
|
Thu, 30 Mar 2000 19:44:11 +0200 |
nipkow |
the simplification rules returned from TFL are now paired with the row they
|
file |
diff |
annotate
|
Mon, 20 Mar 2000 11:15:28 +0100 |
paulson |
replaced best_tac by force_tac, allowing some arithmetic reasoning
|
file |
diff |
annotate
|
Wed, 18 Aug 1999 18:44:20 +0200 |
paulson |
from Konrad: support for schematic definitions
|
file |
diff |
annotate
|
Fri, 30 Apr 1999 18:08:58 +0200 |
wenzelm |
tuned defer_recdef interfaces;
|
file |
diff |
annotate
|
Tue, 27 Apr 1999 10:52:25 +0200 |
wenzelm |
proper quiet_mode;
|
file |
diff |
annotate
|
Fri, 23 Apr 1999 12:23:21 +0200 |
paulson |
Now for recdefs that omit the WF relation;
|
file |
diff |
annotate
|
Thu, 22 Apr 1999 12:49:00 +0200 |
wenzelm |
Theory.requires changed to "Recdef" and moved to HOL/Tools/recdef_package.ML;
|
file |
diff |
annotate
|
Tue, 20 Apr 1999 15:19:52 +0200 |
wenzelm |
temporarily reverted to 1.24;
|
file |
diff |
annotate
|
Fri, 16 Apr 1999 14:43:26 +0200 |
wenzelm |
Sign.base_name fid;
|
file |
diff |
annotate
|
Wed, 14 Apr 1999 19:07:39 +0200 |
wenzelm |
quiet_mode;
|
file |
diff |
annotate
|
Wed, 17 Mar 1999 17:20:36 +0100 |
wenzelm |
Theory.sign_of;
|
file |
diff |
annotate
|
Wed, 10 Mar 1999 10:43:59 +0100 |
paulson |
allow meta_outer to do nothing
|
file |
diff |
annotate
|
Wed, 25 Nov 1998 14:04:05 +0100 |
wenzelm |
replaced prs by writeln;
|
file |
diff |
annotate
|
Tue, 30 Jun 1998 20:57:46 +0200 |
berghofe |
Removed structure Prod_Syntax.
|
file |
diff |
annotate
|
Wed, 27 May 1998 12:21:39 +0200 |
paulson |
Changed require to requires for MLWorks
|
file |
diff |
annotate
|
Wed, 29 Apr 1998 11:33:06 +0200 |
wenzelm |
Theory.require;
|
file |
diff |
annotate
|
Fri, 10 Apr 1998 13:40:29 +0200 |
paulson |
can prove the empty relation to be WF
|
file |
diff |
annotate
|
Mon, 03 Nov 1997 12:36:48 +0100 |
wenzelm |
CLASET';
|
file |
diff |
annotate
|
Thu, 23 Oct 1997 12:47:59 +0200 |
wenzelm |
Sign.stamp_names_of;
|
file |
diff |
annotate
|
Fri, 17 Oct 1997 18:14:48 +0200 |
wenzelm |
adapted to qualified names;
|
file |
diff |
annotate
|