| Mon, 08 Mar 2004 12:17:43 +0100 |
ballarin |
Bug-fixes for transitivity reasoner.
|
file |
diff |
annotate
|
| Mon, 30 Sep 2002 16:14:02 +0200 |
berghofe |
Adapted to new simplifier.
|
file |
diff |
annotate
|
| Mon, 30 Sep 2002 15:44:21 +0200 |
nipkow |
modified induct method
|
file |
diff |
annotate
|
| Thu, 06 Dec 2001 00:40:19 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 01 Dec 2001 18:52:32 +0100 |
wenzelm |
renamed class "term" to "type" (actually "HOL.type");
|
file |
diff |
annotate
|
| Mon, 22 Oct 2001 11:54:22 +0200 |
paulson |
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
|
file |
diff |
annotate
|
| Fri, 05 Oct 2001 21:52:39 +0200 |
wenzelm |
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
|
file |
diff |
annotate
|
| Wed, 03 Oct 2001 20:54:16 +0200 |
wenzelm |
tuned parentheses in relational expressions;
|
file |
diff |
annotate
|
| Tue, 04 Sep 2001 21:10:57 +0200 |
wenzelm |
renamed "antecedent" case to "rule_context";
|
file |
diff |
annotate
|
| Mon, 06 Aug 2001 13:43:24 +0200 |
nipkow |
turned translation for 1::nat into def.
|
file |
diff |
annotate
|
| Thu, 21 Dec 2000 10:16:07 +0100 |
paulson |
re-orientation of 0=... (no idea why the backslashes have changed too)
|
file |
diff |
annotate
|
| Sat, 04 Nov 2000 18:41:37 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 23 Oct 2000 22:17:55 +0200 |
wenzelm |
intro_classes by default;
|
file |
diff |
annotate
|
| Thu, 19 Oct 2000 21:22:44 +0200 |
wenzelm |
improved typedef;
|
file |
diff |
annotate
|
| Wed, 18 Oct 2000 23:28:33 +0200 |
wenzelm |
Multisets (from HOL/Induct/Multiset and friends);
|
file |
diff |
annotate
|