src/HOL/Option.ML
1997-12-24 ago New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
1997-11-04 ago added the, option_map, and case analysis theorems
1997-11-03 ago expand_option_case -> split_option_case
1997-10-30 ago For each datatype `t' there is now a theorem `split_t_case' of the form
1997-05-26 ago Deleted option_case_tac because exhaust_tac performs a similar function.
1997-05-22 ago Deleted obsolete proofs. But option_case_tac will be obsolete too
1997-04-11 ago Yet more fast_tac->blast_tac, and other tidying
1996-10-07 ago Removed commands made redundant by new one-point rules
1996-09-26 ago Ran expandshort
1996-09-24 ago Moved Option out of IOA into core HOL