src/HOL/Option.thy
2017-08-07 blanchet 2017-08-07 tuning imports
2016-08-10 nipkow 2016-08-10 "split add" -> "split"
2016-06-22 wenzelm 2016-06-22 bundle lifting_syntax;
2016-05-31 eberlm 2016-05-31 Added code generation for PMFs
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-11-11 Andreas Lochbihler 2015-11-11 add various lemmas
2015-08-31 wenzelm 2015-08-31 proper qualified naming;
2015-08-31 wenzelm 2015-08-31 misc tuning and modernization;
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-02-11 Andreas Lochbihler 2015-02-11 more transfer rules
2015-02-11 Andreas Lochbihler 2015-02-11 add lemmas about functions on option
2015-02-11 Andreas Lochbihler 2015-02-11 tuned proof
2014-11-07 traytel 2014-11-07 more complete fp_sugars for sum and prod; tuned; removed theorem duplicates; removed obsolete Lifting_{Option,Product,Sum} theories
2014-11-04 lammich 2014-11-04 Added Option.bind_split{,_asm,s}
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-09-11 blanchet 2014-09-11 updated news
2014-09-03 blanchet 2014-09-03 tuned imports
2014-09-01 blanchet 2014-09-01 renamed BNF theories
2014-09-01 blanchet 2014-09-01 renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
2014-05-30 blanchet 2014-05-30 tuned whitespace, to make datatype definitions slightly less intimidating
2014-05-26 blanchet 2014-05-26 got rid of '=:' squiggly
2014-03-03 blanchet 2014-03-03 rationalized internals
2014-02-17 blanchet 2014-02-17 renamed 'datatype_new_compat' to 'datatype_compat'
2014-02-16 blanchet 2014-02-16 folded 'Option.set' into BNF-generated 'set_option'
2014-02-14 blanchet 2014-02-14 renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)
2014-02-14 blanchet 2014-02-14 merged 'Option.map' and 'Option.map_option'
2014-02-12 blanchet 2014-02-12 tuning
2014-02-12 blanchet 2014-02-12 adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems * * * more transition of 'xxx_rec' to 'rec_xxx' and same for case * * * compile * * * 'rename_tac's to avoid referring to generated names * * * more robust scripts with 'rename_tac' * * * 'where' -> 'of' * * * 'where' -> 'of' * * * renamed 'xxx_rec' to 'rec_xxx'
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2014-02-12 blanchet 2014-02-12 compatibility names
2014-02-12 blanchet 2014-02-12 use new selector support to define 'the', 'hd', 'tl'
2014-02-12 blanchet 2014-02-12 transformed 'option' and 'list' into new-style datatypes (but register them as old-style as well) * * * compile * * * tuned imports to prevent merge issues in 'Main'
2014-01-24 blanchet 2014-01-24 killed 'More_BNFs' by moving its various bits where they (now) belong
2014-01-20 blanchet 2014-01-20 swapped dependencies of 'Finite_Set' and 'Option' (to move BNF up)
2013-09-26 lammich 2013-09-26 Added symmetric code_unfold-lemmas for null and is_none
2013-08-13 kuncar 2013-08-13 move useful lemmas to Main
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