| 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
|
| Thu, 24 Jul 1997 11:13:12 +0200 |
nipkow |
Replaced clumsy rewriting by the new function simplify on thms.
|
file |
diff |
annotate
|
| Wed, 23 Jul 1997 10:34:18 +0200 |
wenzelm |
tmp fix to accomodate rep_ss changes;
|
file |
diff |
annotate
|
| Fri, 04 Jul 1997 12:32:31 +0200 |
paulson |
Now catches the error of calling tgoalw when there are no goals to prove,
|
file |
diff |
annotate
|
| Mon, 23 Jun 1997 11:33:59 +0200 |
paulson |
Removal of structure Context and its replacement by a theorem list of
|
file |
diff |
annotate
|
| Thu, 05 Jun 1997 13:27:28 +0200 |
paulson |
Numerous simplifications and removal of HOL-isms
|
file |
diff |
annotate
|
| Tue, 03 Jun 1997 11:08:08 +0200 |
paulson |
More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
|
file |
diff |
annotate
|
| Mon, 26 May 1997 12:28:30 +0200 |
paulson |
Now checks the name of the function being defined
|
file |
diff |
annotate
|
| Thu, 22 May 1997 15:13:16 +0200 |
paulson |
New headers and other minor changes
|
file |
diff |
annotate
|
| Wed, 21 May 1997 10:57:38 +0200 |
paulson |
Basis library input/output primitives; currying the induction rule;
|
file |
diff |
annotate
|
| Tue, 20 May 1997 11:49:57 +0200 |
paulson |
Removal of redundant code (unused or already present in Isabelle.
|
file |
diff |
annotate
|
| Fri, 16 May 1997 10:43:44 +0200 |
paulson |
Subst now moved to directory HOL
|
file |
diff |
annotate
|
| Thu, 15 May 1997 12:29:59 +0200 |
paulson |
TFL now integrated with HOL (more work needed)
|
file |
diff |
annotate
|
| Fri, 03 Jan 1997 10:45:31 +0100 |
paulson |
Conversion to Basis Library (using prs instead of output)
|
file |
diff |
annotate
|
| Fri, 18 Oct 1996 12:41:04 +0200 |
paulson |
Konrad Slind's TFL
|
file |
diff |
annotate
|