src/HOL/Option.thy
Sat, 10 Nov 2018 07:57:19 +0000 haftmann clarified status of legacy input abbreviations
Sun, 17 Jun 2018 20:31:51 +0200 nipkow added simp rules
Fri, 20 Apr 2018 07:36:59 +0000 haftmann moved lemma to more appropriate place
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Sun, 26 Nov 2017 21:08:32 +0100 wenzelm more symbols;
Mon, 07 Aug 2017 11:21:11 +0200 blanchet tuning imports
Wed, 10 Aug 2016 09:33:54 +0200 nipkow "split add" -> "split"
Wed, 22 Jun 2016 10:09:20 +0200 wenzelm bundle lifting_syntax;
Tue, 31 May 2016 13:02:44 +0200 eberlm Added code generation for PMFs
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t;
Wed, 11 Nov 2015 09:48:24 +0100 Andreas Lochbihler add various lemmas
Mon, 31 Aug 2015 20:56:24 +0200 wenzelm proper qualified naming;
Mon, 31 Aug 2015 19:34:26 +0200 wenzelm misc tuning and modernization;
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Wed, 11 Feb 2015 15:03:21 +0100 Andreas Lochbihler more transfer rules
Wed, 11 Feb 2015 14:45:10 +0100 Andreas Lochbihler add lemmas about functions on option
Wed, 11 Feb 2015 14:19:46 +0100 Andreas Lochbihler tuned proof
Fri, 07 Nov 2014 11:28:37 +0100 traytel more complete fp_sugars for sum and prod;
Tue, 04 Nov 2014 17:33:08 +0100 lammich Added Option.bind_split{,_asm,s}
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Thu, 11 Sep 2014 19:32:36 +0200 blanchet updated news
Wed, 03 Sep 2014 00:06:26 +0200 blanchet tuned imports
Mon, 01 Sep 2014 16:34:40 +0200 blanchet renamed BNF theories
Mon, 01 Sep 2014 16:17:46 +0200 blanchet renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
Fri, 30 May 2014 12:27:51 +0200 blanchet tuned whitespace, to make datatype definitions slightly less intimidating
Mon, 26 May 2014 16:32:55 +0200 blanchet got rid of '=:' squiggly
Mon, 03 Mar 2014 12:48:20 +0100 blanchet rationalized internals
Mon, 17 Feb 2014 13:31:42 +0100 blanchet renamed 'datatype_new_compat' to 'datatype_compat'
Sun, 16 Feb 2014 18:39:40 +0100 blanchet folded 'Option.set' into BNF-generated 'set_option'
Fri, 14 Feb 2014 07:53:46 +0100 blanchet renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)
Fri, 14 Feb 2014 07:53:46 +0100 blanchet merged 'Option.map' and 'Option.map_option'
Wed, 12 Feb 2014 17:35:59 +0100 blanchet tuning
Wed, 12 Feb 2014 08:37:06 +0100 blanchet adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
Wed, 12 Feb 2014 08:35:57 +0100 blanchet renamed '{prod,sum,bool,unit}_case' to 'case_...'
Wed, 12 Feb 2014 08:35:56 +0100 blanchet compatibility names
Wed, 12 Feb 2014 08:35:56 +0100 blanchet use new selector support to define 'the', 'hd', 'tl'
Wed, 12 Feb 2014 08:35:56 +0100 blanchet transformed 'option' and 'list' into new-style datatypes (but register them as old-style as well)
Fri, 24 Jan 2014 11:51:45 +0100 blanchet killed 'More_BNFs' by moving its various bits where they (now) belong
Mon, 20 Jan 2014 23:34:26 +0100 blanchet swapped dependencies of 'Finite_Set' and 'Option' (to move BNF up)
Thu, 26 Sep 2013 13:37:33 +0200 lammich Added symmetric code_unfold-lemmas for null and is_none
Tue, 13 Aug 2013 15:59:22 +0200 kuncar move useful lemmas to Main
Sun, 23 Jun 2013 21:16:07 +0200 haftmann migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
Fri, 12 Apr 2013 17:21:51 +0200 wenzelm modifiers for classical wrappers operate on Proof.context instead of claset;
Wed, 13 Feb 2013 13:38:52 +0100 haftmann combinator List.those;
Fri, 07 Sep 2012 08:20:18 +0200 haftmann combinator Option.these
Sat, 18 Feb 2012 09:46:58 +0100 krauss added congruence rules for Option.{map|bind}
Tue, 11 Jan 2011 14:12:37 +0100 haftmann "enriched_type" replaces less specific "type_lifting"
Tue, 21 Dec 2010 17:52:23 +0100 haftmann tuned type_lifting declarations
Mon, 06 Dec 2010 09:19:10 +0100 haftmann replace `type_mapper` by the more adequate `type_lifting`
Thu, 18 Nov 2010 17:01:16 +0100 haftmann mapper for option type
Fri, 10 Sep 2010 10:21:25 +0200 haftmann Haskell == is infix, not infixl
Mon, 06 Sep 2010 19:13:10 +0200 wenzelm more antiquotations;
Sun, 05 Sep 2010 21:39:24 +0200 krauss removed duplicate lemma
Sun, 05 Sep 2010 21:39:16 +0200 krauss added Option.bind
Fri, 27 Aug 2010 19:34:23 +0200 haftmann renamed class/constant eq to equal; tuned some instantiations
Mon, 19 Jul 2010 11:55:43 +0200 haftmann Scala: subtle difference in printing strings vs. complex mixfix syntax
Fri, 16 Apr 2010 21:28:09 +0200 wenzelm replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
Wed, 10 Mar 2010 16:53:27 +0100 haftmann split off theory Big_Operators from theory Finite_Set
Wed, 13 Jan 2010 08:56:15 +0100 haftmann some syntax setup for Scala
Tue, 14 Jul 2009 16:27:32 +0200 haftmann prefer code_inline over code_unfold; use code_unfold_post where appropriate
less more (0) -60 tip