src/HOL/Option.thy
2009-03-04 nipkow 2009-03-04 Option.thy
2007-08-07 haftmann 2007-08-07 split off Option theory
2000-05-30 berghofe 2000-05-30 the is now defined using primrec, avoiding explicit use of arbitrary.
1998-09-09 oheimb 1998-09-09 AddIffs[not_None_eq]; made wrapper ospec really safe
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1998-03-24 oheimb 1998-03-24 added o2s
1997-11-10 oheimb 1997-11-10 replaced 8bit characters
1997-11-04 oheimb 1997-11-04 added the, option_map, and case analysis theorems
1996-09-24 nipkow 1996-09-24 Moved Option out of IOA into core HOL