| Mon, 18 Sep 2000 14:10:31 +0200 |
wenzelm |
indicate occurrences of 'handle _';
|
file |
diff |
annotate
|
| Wed, 06 Sep 2000 17:58:37 +0200 |
wenzelm |
fixed structure U;
|
file |
diff |
annotate
|
| Tue, 05 Sep 2000 18:53:21 +0200 |
wenzelm |
proper handling of hints;
|
file |
diff |
annotate
|
| Thu, 31 Aug 2000 09:23:01 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Tue, 29 Aug 2000 15:13:10 +0200 |
nipkow |
*** empty log message ***
|
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
|
| Thu, 13 Jul 2000 23:20:57 +0200 |
wenzelm |
adapted PureThy.add_defs_i;
|
file |
diff |
annotate
|
| Fri, 05 May 2000 22:35:51 +0200 |
wenzelm |
error msg: counting from one (again), in order to be consistent with
|
file |
diff |
annotate
|
| Sat, 15 Apr 2000 17:41:20 +0200 |
nipkow |
mod to error msg
|
file |
diff |
annotate
|
| Fri, 31 Mar 2000 22:01:01 +0200 |
wenzelm |
made SML/XL happy;
|
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
|
| Fri, 17 Mar 2000 15:49:50 +0100 |
paulson |
better error messages, especially for multiple types
|
file |
diff |
annotate
|
| Mon, 13 Mar 2000 13:28:31 +0100 |
wenzelm |
adapted to new PureThy.add_thms etc.;
|
file |
diff |
annotate
|
| Wed, 08 Mar 2000 17:35:08 +0100 |
wenzelm |
tuned error msg: rows counted from 1;
|
file |
diff |
annotate
|
| Thu, 21 Oct 1999 18:46:33 +0200 |
wenzelm |
get_thm;
|
file |
diff |
annotate
|
| Mon, 04 Oct 1999 21:41:09 +0200 |
wenzelm |
renamed 'prefix' to 'prfx' (avoids clash with infix);
|
file |
diff |
annotate
|
| Thu, 19 Aug 1999 15:13:37 +0200 |
paulson |
removed needless comments
|
file |
diff |
annotate
|
| Wed, 18 Aug 1999 18:44:20 +0200 |
paulson |
from Konrad: support for schematic definitions
|
file |
diff |
annotate
|
| Wed, 21 Jul 1999 15:16:32 +0200 |
paulson |
better error message for curried recdefs, etc.
|
file |
diff |
annotate
|
| Mon, 03 May 1999 11:19:08 +0200 |
paulson |
improved error handling
|
file |
diff |
annotate
|
| Fri, 23 Apr 1999 12:23:21 +0200 |
paulson |
Now for recdefs that omit the WF relation;
|
file |
diff |
annotate
|
| Wed, 17 Mar 1999 17:20:36 +0100 |
wenzelm |
Theory.sign_of;
|
file |
diff |
annotate
|
| Tue, 12 Jan 1999 13:54:51 +0100 |
wenzelm |
eliminated tthm type and Attribute structure;
|
file |
diff |
annotate
|
| Wed, 29 Apr 1998 11:33:27 +0200 |
wenzelm |
adapted to new PureThy.add_defs;
|
file |
diff |
annotate
|
| Thu, 20 Nov 1997 12:59:20 +0100 |
wenzelm |
tuned infer_types interface;
|
file |
diff |
annotate
|
| Wed, 12 Nov 1997 16:27:13 +0100 |
wenzelm |
structure BasisLibrary;
|
file |
diff |
annotate
|
| Wed, 05 Nov 1997 11:45:51 +0100 |
wenzelm |
fixed exception OPTION;
|
file |
diff |
annotate
|
| Sat, 01 Nov 1997 13:01:07 +0100 |
paulson |
New way of referring to Basis Library
|
file |
diff |
annotate
|
| Tue, 28 Oct 1997 17:56:57 +0100 |
wenzelm |
PureThy.add_store_defs_i;
|
file |
diff |
annotate
|
| Mon, 20 Oct 1997 11:14:16 +0200 |
wenzelm |
lookup long names of types;
|
file |
diff |
annotate
|
| Fri, 17 Oct 1997 18:14:48 +0200 |
wenzelm |
adapted to qualified names;
|
file |
diff |
annotate
|
| Wed, 01 Oct 1997 18:13:41 +0200 |
wenzelm |
fully qualified names: Theory.add_XXX;
|
file |
diff |
annotate
|
| Thu, 25 Sep 1997 12:24:53 +0200 |
paulson |
Deleted the unused gtake and recoded enumerate to use foldl
|
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, 02 Jun 1997 12:19:01 +0200 |
paulson |
Type inference makes a Const here, perhaps elsewhere?thry.sml
|
file |
diff |
annotate
|
| Mon, 02 Jun 1997 12:17:19 +0200 |
paulson |
poly_tvars allows recdefs to be made without type constraints
|
file |
diff |
annotate
|
| Fri, 30 May 1997 15:55:27 +0200 |
paulson |
Simplified the calling sequence of CONTEXT_REWRITE_RULE
|
file |
diff |
annotate
|
| Tue, 27 May 1997 13:22:30 +0200 |
paulson |
Removal of module Mask and datatype binding with its constructor |->
|
file |
diff |
annotate
|
| Mon, 26 May 1997 12:29:55 +0200 |
paulson |
Now checks the name of the function being defined;
|
file |
diff |
annotate
|
| Thu, 22 May 1997 15:11:56 +0200 |
paulson |
Now the recdef induction rule variables are named u, v, ...
|
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
|
| Thu, 15 May 1997 12:29:59 +0200 |
paulson |
TFL now integrated with HOL (more work needed)
|
file |
diff |
annotate
|
| Fri, 18 Oct 1996 12:41:04 +0200 |
paulson |
Konrad Slind's TFL
|
file |
diff |
annotate
|