src/HOL/Option.thy
changeset 9001 93af64f54bf2
parent 5445 3905974ad555
     1.1 --- a/src/HOL/Option.thy	Tue May 30 16:08:38 2000 +0200
     1.2 +++ b/src/HOL/Option.thy	Tue May 30 18:02:49 2000 +0200
     1.3 @@ -10,21 +10,19 @@
     1.4  
     1.5  datatype 'a option = None | Some 'a
     1.6  
     1.7 -constdefs
     1.8 +consts
     1.9 +  the :: "'a option => 'a"
    1.10 +  o2s :: "'a option => 'a set"
    1.11  
    1.12 -  the		:: "'a option => 'a"
    1.13 - "the == %y. case y of None => arbitrary | Some x => x"
    1.14 +primrec
    1.15 + "the (Some x) = x"
    1.16  
    1.17 +primrec
    1.18 + "o2s  None    = {}"
    1.19 + "o2s (Some x) = {x}"
    1.20 +
    1.21 +constdefs
    1.22    option_map	:: "('a => 'b) => ('a option => 'b option)"
    1.23   "option_map == %f y. case y of None => None | Some x => Some (f x)"
    1.24  
    1.25 -consts
    1.26 -
    1.27 -  o2s	   :: "'a option => 'a set"
    1.28 -
    1.29 -primrec
    1.30 -
    1.31 - "o2s  None    = {}"
    1.32 - "o2s (Some x) = {x}"
    1.33 -
    1.34  end