| Sat, 01 Dec 2001 18:52:32 +0100 |
wenzelm |
renamed class "term" to "type" (actually "HOL.type");
|
file |
diff |
annotate
|
| Fri, 09 Nov 2001 00:09:47 +0100 |
wenzelm |
eliminated old "symbols" syntax, use "xsymbols" instead;
|
file |
diff |
annotate
|
| Sat, 27 Oct 2001 23:16:15 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 19 Oct 2001 22:01:25 +0200 |
wenzelm |
got rid of ML proof scripts for Product_Type;
|
file |
diff |
annotate
|
| Wed, 17 Oct 2001 20:24:03 +0200 |
wenzelm |
proper proof of split_paired_all (presently unused);
|
file |
diff |
annotate
|
| Mon, 15 Oct 2001 20:33:42 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 27 Sep 2001 22:22:58 +0200 |
wenzelm |
renamed "()" to Unity, made local;
|
file |
diff |
annotate
|
| Thu, 09 Aug 2001 10:17:45 +0200 |
oheimb |
added pair_imageI (also as intro rule)
|
file |
diff |
annotate
|
| Wed, 25 Jul 2001 13:13:01 +0200 |
paulson |
partial restructuring to reduce dependence on Axiom of Choice
|
file |
diff |
annotate
|
| Sun, 15 Jul 2001 14:47:28 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 02 Feb 2001 22:18:10 +0100 |
wenzelm |
added hidden internal_split constant;
|
file |
diff |
annotate
|
| Thu, 01 Feb 2001 20:51:48 +0100 |
oheimb |
converted to Isar therory, adding attributes complete_split and split_format
|
file |
diff |
annotate
|
| Mon, 23 Oct 2000 11:14:00 +0200 |
wenzelm |
tuned deps;
|
file |
diff |
annotate
|
| Thu, 12 Oct 2000 18:44:35 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|