| Tue, 30 Jun 1998 20:50:34 +0200 | berghofe | Adapted to new inductive package. | file | diff | annotate |
| Thu, 05 Jun 1997 14:39:22 +0200 | nipkow | Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'. | file | diff | annotate |
| Tue, 03 Jun 1997 10:53:58 +0200 | paulson | New theorem about the cardinality of the powerset (uses exponentiation) | file | diff | annotate |
| Fri, 30 May 1997 15:16:44 +0200 | paulson | Now Divides must be the parent | file | diff | annotate |
| Wed, 06 Mar 1996 14:12:24 +0100 | clasohm | added constdefs section | file | diff | annotate |
| Mon, 04 Mar 1996 14:37:33 +0100 | nipkow | Added a constant UNIV == {x.True} | file | diff | annotate |
| Mon, 05 Feb 1996 21:27:16 +0100 | clasohm | expanded tabs; renamed subtype to typedef; | file | diff | annotate |
| Wed, 29 Nov 1995 16:44:59 +0100 | clasohm | removed quotes from types in consts and syntax sections | file | diff | annotate |
| Fri, 03 Mar 1995 12:02:25 +0100 | clasohm | new version of HOL with curried function application | file | diff | annotate |