Thu, 15 Feb 2001 13:07:03 +0100 |
oheimb |
added missiong word
|
file |
diff |
annotate
|
Wed, 14 Feb 2001 23:17:53 +0100 |
wenzelm |
isatool install handles KDE version 1 or 2;
|
file |
diff |
annotate
|
Tue, 13 Feb 2001 22:51:08 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sun, 11 Feb 2001 16:34:20 +0100 |
wenzelm |
more robust selection of calculational rules;
|
file |
diff |
annotate
|
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
|
Sat, 06 Jan 2001 10:36:19 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
Fri, 05 Jan 2001 18:31:48 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
Wed, 03 Jan 2001 21:21:28 +0100 |
wenzelm |
* Isar/HOL: added 'recdef_tc' command;
|
file |
diff |
annotate
|
Mon, 01 Jan 2001 11:50:31 +0100 |
paulson |
Hyperreal
|
file |
diff |
annotate
|
Fri, 22 Dec 2000 18:20:55 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Wed, 13 Dec 2000 16:21:40 +0100 |
wenzelm |
* print modes "brackets" and "no_brackets" control output of nested =>
|
file |
diff |
annotate
|
Thu, 07 Dec 2000 22:35:25 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Wed, 06 Dec 2000 13:59:42 +0100 |
bauerg |
HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse" function;
|
file |
diff |
annotate
|
Thu, 30 Nov 2000 20:18:00 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Thu, 30 Nov 2000 20:03:39 +0100 |
wenzelm |
misc;
|
file |
diff |
annotate
|
Thu, 23 Nov 2000 21:29:35 +0100 |
wenzelm |
* HOL: syntax or "abs";
|
file |
diff |
annotate
|