src/HOL/Option.ML
1999-07-19 paulson 1999-07-19 getting rid of qed_goal
1998-09-21 oheimb 1998-09-21 added addD2, addE2, addSD2, and addSE2 added not_Some_eq, also to simpset() and claset()
1998-09-09 oheimb 1998-09-09 AddIffs[not_None_eq]; made wrapper ospec really safe
1998-08-12 oheimb 1998-08-12 added ospec AddIffs [elem_o2s]
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1998-04-27 oheimb 1998-04-27 added option_map_eq_Some via AddIffs
1998-04-07 oheimb 1998-04-07 replaced option_map_SomeD by option_map_eq_Some (RS iffD1) added option_map_eq_Some to simpset(), option_map_eq_Some RS iffD1 to claset()
1998-03-24 oheimb 1998-03-24 added o2s
1997-12-24 paulson 1997-12-24 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
1997-11-04 oheimb 1997-11-04 added the, option_map, and case analysis theorems
1997-11-03 nipkow 1997-11-03 expand_option_case -> split_option_case
1997-10-30 nipkow 1997-10-30 For each datatype `t' there is now a theorem `split_t_case' of the form P(t_case f1 ... fn x) = ((!y1 ... ym1. x = C1 y1 ... ym1 --> P(f1 y1 ... ym1))& ... (!y1 ... ymn. x = Cn y1 ... ymn --> P(f1 y1 ... ymn))) The simplifier now reduces !x. (..x.. & x = t & ..x..) --> P x to (..t.. & ..t..) --> P t (and similarly for t=x).
1997-05-26 paulson 1997-05-26 Deleted option_case_tac because exhaust_tac performs a similar function. Deleted the duplicate proof of expand_option_case...
1997-05-22 paulson 1997-05-22 Deleted obsolete proofs. But option_case_tac will be obsolete too
1997-04-11 paulson 1997-04-11 Yet more fast_tac->blast_tac, and other tidying
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