src/HOL/Option.ML

--- a/src/HOL/Option.ML	Wed Oct 29 16:03:19 1997 +0100
+++ b/src/HOL/Option.ML	Thu Oct 30 09:45:03 1997 +0100
@@ -6,11 +6,4 @@
 Derived rules
 *)
 
-open Option;
-
-goal Option.thy "P(case opt of None => a | Some(x) => b x) = \
-\                ((opt = None --> P a) & (!x. opt = Some x --> P(b x)))";
-by (option.induct_tac "opt" 1);
-by (Simp_tac 1);
-by (Asm_full_simp_tac 1);
-qed "expand_option_case";
+val expand_option_case = split_option_case;