src/HOL/Option.ML
changeset 9001 93af64f54bf2
parent 8442 96023903c2df
child 9343 1c4754938980
     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";