src/HOL/Option.thy
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
Tue, 14 Jul 2009 10:54:04 +0200 haftmann code attributes use common underscore convention
Thu, 14 May 2009 15:09:47 +0200 haftmann preprocessing must consider eq
Sat, 09 May 2009 07:25:22 +0200 nipkow lemmas by Andreas Lochbihler
Fri, 06 Mar 2009 20:30:17 +0100 haftmann moved instance option :: finite to Option.thy
Wed, 04 Mar 2009 11:48:52 +0100 nipkow Option.thy
Tue, 07 Aug 2007 10:03:25 +0200 haftmann split off Option theory
Tue, 30 May 2000 18:02:49 +0200 berghofe the is now defined using primrec, avoiding explicit use of arbitrary.
Wed, 09 Sep 1998 17:23:42 +0200 oheimb AddIffs[not_None_eq];
Fri, 24 Jul 1998 13:03:20 +0200 berghofe Adapted to new datatype package.
Tue, 24 Mar 1998 15:51:37 +0100 oheimb added o2s
Mon, 10 Nov 1997 14:57:31 +0100 oheimb replaced 8bit characters
Tue, 04 Nov 1997 20:48:38 +0100 oheimb added the, option_map, and case analysis theorems
Tue, 24 Sep 1996 09:02:34 +0200 nipkow Moved Option out of IOA into core HOL
less more (0) tip