| Wed, 25 Jul 2001 17:58:26 +0200 |
paulson |
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
|
file |
diff |
annotate
|
| Wed, 07 Feb 2001 20:57:03 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 23 Oct 2000 11:15:52 +0200 |
wenzelm |
isatool unsymbolize;
|
file |
diff |
annotate
|
| Mon, 23 Oct 2000 11:14:43 +0200 |
wenzelm |
added type_definitionI;
|
file |
diff |
annotate
|
| Fri, 20 Oct 2000 19:46:53 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 19 Oct 2000 21:22:05 +0200 |
wenzelm |
added theory for HOL type definitions;
|
file |
diff |
annotate
|
| Thu, 07 Sep 2000 20:52:02 +0200 |
wenzelm |
added linorder_cases;
|
file |
diff |
annotate
|
| Tue, 05 Oct 1999 15:29:46 +0200 |
berghofe |
Added attribute rulify_prems (useful for modifying premises of introduction
|
file |
diff |
annotate
|
| Mon, 04 Oct 1999 21:46:49 +0200 |
wenzelm |
Tools/typedef_package.ML;
|
file |
diff |
annotate
|
| Fri, 13 Nov 1998 13:27:03 +0100 |
paulson |
no longer loads Fun so that the Fun proofs can use equalities.thy
|
file |
diff |
annotate
|
| Mon, 05 Feb 1996 21:27:16 +0100 |
clasohm |
expanded tabs; renamed subtype to typedef;
|
file |
diff |
annotate
|
| Fri, 03 Mar 1995 12:02:25 +0100 |
clasohm |
new version of HOL with curried function application
|
file |
diff |
annotate
|