| Tue, 10 Oct 2006 13:59:13 +0200 |
haftmann |
gen_rem(s) abandoned in favour of remove / subtract
|
file |
diff |
annotate
|
| Fri, 15 Sep 2006 22:56:13 +0200 |
wenzelm |
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
|
file |
diff |
annotate
|
| Wed, 19 Jul 2006 12:11:57 +0200 |
wenzelm |
Sign.infer_types: Name.context;
|
file |
diff |
annotate
|
| Tue, 11 Jul 2006 12:17:16 +0200 |
wenzelm |
replaced Term.variant(list) by Name.variant(_list);
|
file |
diff |
annotate
|
| Sat, 08 Jul 2006 12:54:50 +0200 |
wenzelm |
tuned interface;
|
file |
diff |
annotate
|
| Mon, 19 Jun 2006 22:06:36 +0200 |
wenzelm |
refrain from reforming TFL -- back to previous revision;
|
file |
diff |
annotate
|
| Mon, 19 Jun 2006 20:21:30 +0200 |
wenzelm |
eliminated freeze/varify in favour of Variable.import/export/trade;
|
file |
diff |
annotate
|
| Tue, 13 Jun 2006 23:41:39 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 06 Apr 2006 16:13:17 +0200 |
haftmann |
cleanup in typedef/datatype package
|
file |
diff |
annotate
|
| Wed, 15 Feb 2006 21:34:55 +0100 |
wenzelm |
removed distinct, renamed gen_distinct to distinct;
|
file |
diff |
annotate
|
| Tue, 07 Feb 2006 19:56:56 +0100 |
wenzelm |
adapted Sign.infer_types;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2006 17:14:06 +0100 |
wenzelm |
sane ERROR handling;
|
file |
diff |
annotate
|
| Tue, 06 Dec 2005 09:04:09 +0100 |
haftmann |
re-oriented some result tuples in PureThy
|
file |
diff |
annotate
|
| Wed, 16 Nov 2005 17:45:22 +0100 |
wenzelm |
Term.betapply;
|
file |
diff |
annotate
|
| Sat, 17 Sep 2005 18:11:25 +0200 |
wenzelm |
removed obsolete BasisLibrary;
|
file |
diff |
annotate
|
| Thu, 08 Sep 2005 16:09:23 +0200 |
haftmann |
introduces some modern-style AList operations
|
file |
diff |
annotate
|
| Thu, 14 Jul 2005 19:28:38 +0200 |
wenzelm |
replaced itlist by fold_rev;
|
file |
diff |
annotate
|
| Mon, 20 Jun 2005 22:14:20 +0200 |
wenzelm |
avoid identifier 'Name';
|
file |
diff |
annotate
|
| Fri, 04 Mar 2005 15:07:34 +0100 |
skalberg |
Removed practically all references to Library.foldr.
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Sat, 29 May 2004 14:59:24 +0200 |
wenzelm |
Sign.infer_types: Sign.pp;
|
file |
diff |
annotate
|
| Fri, 17 Oct 2003 11:03:48 +0200 |
paulson |
improved tracing
|
file |
diff |
annotate
|
| Fri, 03 Oct 2003 12:36:16 +0200 |
paulson |
added a comment
|
file |
diff |
annotate
|
| Wed, 01 Oct 2003 11:02:36 +0200 |
berghofe |
Fixed inefficiency in post_definition by adding weak case congruence
|
file |
diff |
annotate
|
| Wed, 20 Feb 2002 00:53:53 +0100 |
wenzelm |
Symbol.bump_string;
|
file |
diff |
annotate
|
| Fri, 28 Sep 2001 19:23:35 +0200 |
wenzelm |
prove: ``strict'' argument;
|
file |
diff |
annotate
|
| Wed, 25 Jul 2001 18:21:01 +0200 |
paulson |
defer_recdef (lazyR_def) now looks for theorem Hilbert_Choice.tfl_some
|
file |
diff |
annotate
|
| Wed, 03 Jan 2001 21:20:40 +0100 |
wenzelm |
renamed .sml files to .ML;
|
file |
diff |
annotate
|