| Sun, 11 Feb 2001 13:26:23 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 10 Feb 2001 08:48:10 +0100 |
ballarin |
Updates to HOL/Algebra:
|
file |
diff |
annotate
|
| Mon, 05 Feb 2001 14:31:49 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 04 Feb 2001 19:40:06 +0100 |
wenzelm |
* no_document ML operator temporarily disables LaTeX document
|
file |
diff |
annotate
|
| Sat, 03 Feb 2001 15:20:55 +0100 |
wenzelm |
HOL: inductive package no longer splits induction rule aggressively,
|
file |
diff |
annotate
|
| Thu, 01 Feb 2001 20:42:34 +0100 |
wenzelm |
* Pure: 'thms_containing' now takes actual terms as arguments;
|
file |
diff |
annotate
|
| Tue, 30 Jan 2001 14:21:50 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 24 Jan 2001 21:01:47 +0100 |
wenzelm |
* Document preparation: renamed standard symbols \<ll> to \<lless> and
|
file |
diff |
annotate
|
| Tue, 23 Jan 2001 18:05:53 +0100 |
wenzelm |
added HOL-Unix example;
|
file |
diff |
annotate
|
| Sat, 20 Jan 2001 00:01:40 +0100 |
wenzelm |
*** empty log message ***
|
file |
diff |
annotate
|
| Tue, 16 Jan 2001 00:37:41 +0100 |
wenzelm |
* HOL/datatype: induction rule for arbitrarily branching datatypes is
|
file |
diff |
annotate
|
| Thu, 11 Jan 2001 12:49:48 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Wed, 10 Jan 2001 20:21:11 +0100 |
wenzelm |
isatool unsymbolize;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2001 20:18:55 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2001 13:30:25 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|