| Tue, 07 Aug 2007 10:03:25 +0200 | haftmann | split off Option theory | file | diff | annotate |
| Tue, 30 May 2000 18:02:49 +0200 | berghofe | the is now defined using primrec, avoiding explicit use of arbitrary. | file | diff | annotate |
| Wed, 09 Sep 1998 17:23:42 +0200 | oheimb | AddIffs[not_None_eq]; | file | diff | annotate |
| Fri, 24 Jul 1998 13:03:20 +0200 | berghofe | Adapted to new datatype package. | file | diff | annotate |
| Tue, 24 Mar 1998 15:51:37 +0100 | oheimb | added o2s | file | diff | annotate |
| Mon, 10 Nov 1997 14:57:31 +0100 | oheimb | replaced 8bit characters | file | diff | annotate |
| Tue, 04 Nov 1997 20:48:38 +0100 | oheimb | added the, option_map, and case analysis theorems | file | diff | annotate |
| Tue, 24 Sep 1996 09:02:34 +0200 | nipkow | Moved Option out of IOA into core HOL | file | diff | annotate |