src/HOL/Option.ML
1996-10-07 paulson 1996-10-07 Removed commands made redundant by new one-point rules
1996-09-26 paulson 1996-09-26 Ran expandshort
1996-09-24 nipkow 1996-09-24 Moved Option out of IOA into core HOL