| Thu, 07 Sep 2000 21:12:49 +0200 |
wenzelm |
tuned ML code (the_context, bind_thms(s));
|
file |
diff |
annotate
|
| Fri, 30 Jun 2000 12:51:30 +0200 |
paulson |
removal of batch-style proofs
|
file |
diff |
annotate
|
| Wed, 28 Jun 2000 10:57:35 +0200 |
paulson |
FORCED TO RENAME "W" DUE TO COMPOSE VARIABLE-CLASH BUG
|
file |
diff |
annotate
|
| Mon, 28 Dec 1998 16:59:28 +0100 |
paulson |
new inductive, datatype and primrec packages, etc.
|
file |
diff |
annotate
|
| Wed, 15 Jul 1998 14:13:18 +0200 |
paulson |
More tidying and removal of "\!\!... from Goal commands
|
file |
diff |
annotate
|
| Mon, 22 Jun 1998 17:12:27 +0200 |
wenzelm |
isatool fixgoal;
|
file |
diff |
annotate
|
| Mon, 03 Nov 1997 12:24:13 +0100 |
wenzelm |
isatool fixclasimp;
|
file |
diff |
annotate
|
| Thu, 16 Oct 1997 13:38:47 +0200 |
wenzelm |
transfer InfDatatype.thy Limit_VfromE;
|
file |
diff |
annotate
|
| Fri, 03 Jan 1997 15:01:55 +0100 |
paulson |
Implicit simpsets and clasets for FOL and ZF
|
file |
diff |
annotate
|
| Tue, 30 Jan 1996 13:42:57 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| Fri, 16 Dec 1994 17:44:09 +0100 |
lcp |
Added Limit_csucc from CardinalArith
|
file |
diff |
annotate
|
| Thu, 08 Dec 1994 14:18:31 +0100 |
lcp |
UN_upper_cardinal: updated to refer to Card_le_imp_lepoll
|
file |
diff |
annotate
|
| Wed, 07 Dec 1994 13:12:04 +0100 |
clasohm |
added qed and qed_goal[w]
|
file |
diff |
annotate
|
| Thu, 03 Nov 1994 12:43:42 +0100 |
lcp |
ZF/InfDatatype/fun_Vcsucc: removed use of PiE
|
file |
diff |
annotate
|
| Tue, 16 Aug 1994 19:03:45 +0200 |
lcp |
ZF/Finite: added the finite function space, A-||>B
|
file |
diff |
annotate
|
| Mon, 15 Aug 1994 18:15:09 +0200 |
lcp |
ZF/InfDatatype: simplified, extended results for infinite branching
|
file |
diff |
annotate
|
| Fri, 12 Aug 1994 18:45:33 +0200 |
lcp |
for infinite datatypes with arbitrary index sets
|
file |
diff |
annotate
|
| Fri, 12 Aug 1994 12:51:34 +0200 |
lcp |
installation of new inductive/datatype sections
|
file |
diff |
annotate
|
| Wed, 27 Jul 1994 15:33:42 +0200 |
lcp |
Addition of infinite branching datatypes
|
file |
diff |
annotate
|