| changeset 9001 | 93af64f54bf2 |
| parent 8442 | 96023903c2df |
| child 9343 | 1c4754938980 |
--- a/src/HOL/Option.ML Tue May 30 16:08:38 2000 +0200 +++ b/src/HOL/Option.ML Tue May 30 18:02:49 2000 +0200 @@ -42,16 +42,6 @@ qed "option_caseE"; -section "the"; - -Goalw [the_def] "the (Some x) = x"; -by (Simp_tac 1); -qed "the_Some"; - -Addsimps [the_Some]; - - - section "option_map"; Goalw [option_map_def] "option_map f None = None";