Fri, 06 Mar 2009 20:30:17 +0100 |
haftmann |
moved instance option :: finite to Option.thy
|
file |
diff |
annotate
|
Wed, 04 Mar 2009 11:48:52 +0100 |
nipkow |
Option.thy
|
file |
diff |
annotate
|
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
|