src/HOL/Option.thy
changeset 4133 0a08c2b9b1ed
parent 2019 b45d9f2042e0
child 4192 c38ab5af38b5
     1.1 --- a/src/HOL/Option.thy	Tue Nov 04 20:47:38 1997 +0100
     1.2 +++ b/src/HOL/Option.thy	Tue Nov 04 20:48:38 1997 +0100
     1.3 @@ -7,5 +7,15 @@
     1.4  *)
     1.5  
     1.6  Option = Arith +
     1.7 +
     1.8  datatype 'a option = None | Some 'a
     1.9 +
    1.10 +constdefs
    1.11 +
    1.12 +  the		:: "'a option => 'a"
    1.13 + "the  %y. case y of None => arbitrary | Some x => x"
    1.14 +
    1.15 +  option_map	:: "('a => 'b) => ('a option => 'b option)"
    1.16 + "option_map  %f y. case y of None => None | Some x => Some (f x)"
    1.17 +
    1.18  end