| Thu, 14 Jul 2005 19:28:37 +0200 |
wenzelm |
replaced itlist by fold_rev;
|
file |
diff |
annotate
|
| Sun, 05 Jun 2005 23:07:25 +0200 |
wenzelm |
Type.freeze;
|
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
|
| Thu, 02 Sep 2004 14:50:00 +0200 |
dixon |
added code to make use of case splitting to prove the specification equations for recursive definitions.
|
file |
diff |
annotate
|
| Fri, 20 Aug 2004 12:20:09 +0200 |
paulson |
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
|
file |
diff |
annotate
|
| Fri, 17 Oct 2003 11:03:48 +0200 |
paulson |
improved tracing
|
file |
diff |
annotate
|
| Tue, 13 Aug 2002 22:01:53 +0200 |
nipkow |
arith_tac should not produce counter example
|
file |
diff |
annotate
|
| Thu, 13 Dec 2001 16:48:07 +0100 |
nipkow |
Terminator now uses arith_tac as well.
|
file |
diff |
annotate
|
| Mon, 03 Dec 2001 11:47:29 +0100 |
wenzelm |
HOLogic.read_cterm;
|
file |
diff |
annotate
|
| Sun, 14 Oct 2001 22:15:07 +0200 |
wenzelm |
moved rulify to ObjectLogic;
|
file |
diff |
annotate
|
| Fri, 28 Sep 2001 19:23:35 +0200 |
wenzelm |
prove: ``strict'' argument;
|
file |
diff |
annotate
|
| Fri, 02 Feb 2001 22:21:06 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 03 Jan 2001 21:20:40 +0100 |
wenzelm |
renamed .sml files to .ML;
|
file |
diff |
annotate
|