| Sun, 15 Nov 2009 00:23:26 +0100 |
wenzelm |
properly inlined @{lemma} antiqutations -- might also reduce proof terms a bit;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 23:56:33 +0100 |
wenzelm |
eliminated some old folds;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 17:58:26 +0100 |
wenzelm |
standardized filter/filter_out;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 16:59:12 +0100 |
wenzelm |
modernized some structure names;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 14:54:14 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 17:34:00 +0100 |
wenzelm |
normalized basic type abbreviations;
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 16:02:43 +0100 |
wenzelm |
avoid structure alias;
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 12:02:56 +0200 |
haftmann |
curried union as canonical list operation
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 08:16:25 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 08:14:38 +0200 |
haftmann |
dropped redundant gen_ prefix
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 16:13:01 +0200 |
haftmann |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 00:36:12 +0200 |
wenzelm |
standardized basic operations on type option;
|
file |
diff |
annotate
|
| Sun, 18 Oct 2009 20:53:40 +0200 |
wenzelm |
removed some unreferenced material;
|
file |
diff |
annotate
|
| Fri, 16 Oct 2009 10:55:07 +0200 |
wenzelm |
tuned white space;
|
file |
diff |
annotate
|
| Fri, 16 Oct 2009 10:45:10 +0200 |
wenzelm |
local channels for tracing/debugging;
|
file |
diff |
annotate
|
| Thu, 15 Oct 2009 23:28:10 +0200 |
wenzelm |
replaced String.concat by implode;
|
file |
diff |
annotate
|
| Mon, 07 Sep 2009 17:02:15 +0100 |
paulson |
Fixed a few problems with the method metisFT
|
file |
diff |
annotate
|
| Mon, 07 Sep 2009 13:19:09 +0100 |
paulson |
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
|
file |
diff |
annotate
|
| Mon, 07 Sep 2009 10:04:17 +0100 |
paulson |
conflict resolution possibly
|
file |
diff |
annotate
|
| Fri, 04 Sep 2009 11:37:24 +0100 |
paulson |
New method, metisFT: a fully-typed proof search that should eliminate type errors during reconstruction
|
file |
diff |
annotate
|
| Fri, 28 Aug 2009 21:04:03 +0200 |
wenzelm |
modernized messages -- eliminated ctyp/cterm operations;
|
file |
diff |
annotate
|
| Wed, 29 Jul 2009 19:35:10 +0200 |
wenzelm |
Meson.first_order_resolve: avoid handle _;
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 01:03:18 +0200 |
wenzelm |
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
|
file |
diff |
annotate
|
| Wed, 15 Jul 2009 23:48:21 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Mon, 06 Jul 2009 21:24:30 +0200 |
wenzelm |
structure Thm: less pervasive names;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2009 23:50:05 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2009 19:58:26 +0100 |
wenzelm |
unified type Proof.method and pervasive METHOD combinators;
|
file |
diff |
annotate
|
| Sun, 08 Mar 2009 17:05:43 +0100 |
wenzelm |
more explicit warning message;
|
file |
diff |
annotate
|
| Sun, 01 Mar 2009 23:36:12 +0100 |
wenzelm |
use long names for old-style fold combinators;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 00:08:13 +0100 |
wenzelm |
use regular Term.add_vars, Term.add_frees etc.;
|
file |
diff |
annotate
|