Deleted option_case_tac because exhaust_tac performs a similar function.
Deleted the duplicate proof of expand_option_case...
--- a/src/HOL/Option.ML Mon May 26 12:39:57 1997 +0200
+++ b/src/HOL/Option.ML Mon May 26 12:40:51 1997 +0200
@@ -8,26 +8,9 @@
open Option;
-val opt_exhaustion = #nchotomy (the (datatype_info Option.thy "option"))
- RS spec;
-
-(*---------------------------------------------------------------------------
- * Do a case analysis on something of type 'a option.
- *---------------------------------------------------------------------------*)
-
-fun option_case_tac t =
- (cut_inst_tac [("x",t)] opt_exhaustion
- THEN' etac disjE
- THEN' rotate_tac ~1
- THEN' Asm_full_simp_tac
- THEN' etac exE
- THEN' rotate_tac ~1
- THEN' Asm_full_simp_tac);
-
-
-goal Option.thy "P(case opt of None => a | Some(x) => b(x)) = \
-\ ((opt = None --> P a) & (!x. opt = Some x --> P(b(x))))";
+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";
+qed "expand_option_case";