| 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
|