src/HOL/Option.thy
2013-06-23 haftmann 2013-06-23 migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
2013-04-12 wenzelm 2013-04-12 modifiers for classical wrappers operate on Proof.context instead of claset;
2013-02-13 haftmann 2013-02-13 combinator List.those; simprule for case distinction on Option.map expression
2012-09-07 haftmann 2012-09-07 combinator Option.these
2012-02-18 krauss 2012-02-18 added congruence rules for Option.{map|bind}
2011-01-11 haftmann 2011-01-11 "enriched_type" replaces less specific "type_lifting"
2010-12-21 haftmann 2010-12-21 tuned type_lifting declarations
2010-12-06 haftmann 2010-12-06 replace `type_mapper` by the more adequate `type_lifting`
2010-11-18 haftmann 2010-11-18 mapper for option type
2010-09-10 haftmann 2010-09-10 Haskell == is infix, not infixl
2010-09-06 wenzelm 2010-09-06 more antiquotations;
2010-09-05 krauss 2010-09-05 removed duplicate lemma
2010-09-05 krauss 2010-09-05 added Option.bind
2010-08-27 haftmann 2010-08-27 renamed class/constant eq to equal; tuned some instantiations
2010-07-19 haftmann 2010-07-19 Scala: subtle difference in printing strings vs. complex mixfix syntax
2010-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-03-10 haftmann 2010-03-10 split off theory Big_Operators from theory Finite_Set
2010-01-13 haftmann 2010-01-13 some syntax setup for Scala
2009-07-14 haftmann 2009-07-14 prefer code_inline over code_unfold; use code_unfold_post where appropriate
2009-07-14 haftmann 2009-07-14 code attributes use common underscore convention
2009-05-14 haftmann 2009-05-14 preprocessing must consider eq
2009-05-09 nipkow 2009-05-09 lemmas by Andreas Lochbihler
2009-03-06 haftmann 2009-03-06 moved instance option :: finite to 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