src/HOL/Option.thy

 
 Option = Datatype +
 
 datatype 'a option = None | Some 'a
 
+consts
+  the :: "'a option => 'a"
+  o2s :: "'a option => 'a set"
+
+primrec
+ "the (Some x) = x"
+
+primrec
+ "o2s  None    = {}"
+ "o2s (Some x) = {x}"
+
 constdefs
-
-  the		:: "'a option => 'a"
- "the == %y. case y of None => arbitrary | Some x => x"
-
   option_map	:: "('a => 'b) => ('a option => 'b option)"
  "option_map == %f y. case y of None => None | Some x => Some (f x)"
 
-consts
-
-  o2s	   :: "'a option => 'a set"
-
-primrec
-
- "o2s  None    = {}"
- "o2s (Some x) = {x}"
-
 end