1.1 --- a/src/HOL/Option.ML	Tue May 30 16:08:38 2000 +0200
     1.2 +++ b/src/HOL/Option.ML	Tue May 30 18:02:49 2000 +0200
     1.3 @@ -42,16 +42,6 @@
     1.4  qed "option_caseE";
     1.5  
     1.6  
     1.7 -section "the";
     1.8 -
     1.9 -Goalw [the_def] "the (Some x) = x";
    1.10 -by (Simp_tac 1);
    1.11 -qed "the_Some";
    1.12 -
    1.13 -Addsimps [the_Some];
    1.14 -
    1.15 -
    1.16 -
    1.17  section "option_map";
    1.18  
    1.19  Goalw [option_map_def] "option_map f None = None";

     2.1 --- a/src/HOL/Option.thy	Tue May 30 16:08:38 2000 +0200
     2.2 +++ b/src/HOL/Option.thy	Tue May 30 18:02:49 2000 +0200
     2.3 @@ -10,21 +10,19 @@
     2.4  
     2.5  datatype 'a option = None | Some 'a
     2.6  
     2.7 +consts
     2.8 +  the :: "'a option => 'a"
     2.9 +  o2s :: "'a option => 'a set"
    2.10 +
    2.11 +primrec
    2.12 + "the (Some x) = x"
    2.13 +
    2.14 +primrec
    2.15 + "o2s  None    = {}"
    2.16 + "o2s (Some x) = {x}"
    2.17 +
    2.18  constdefs
    2.19 -
    2.20 -  the		:: "'a option => 'a"
    2.21 - "the == %y. case y of None => arbitrary | Some x => x"
    2.22 -
    2.23    option_map	:: "('a => 'b) => ('a option => 'b option)"
    2.24   "option_map == %f y. case y of None => None | Some x => Some (f x)"
    2.25  
    2.26 -consts
    2.27 -
    2.28 -  o2s	   :: "'a option => 'a set"
    2.29 -
    2.30 -primrec
    2.31 -
    2.32 - "o2s  None    = {}"
    2.33 - "o2s (Some x) = {x}"
    2.34 -
    2.35  end