# HG changeset patch
# User paulson
# Date 864643251 -7200
# Node ID b3e39a2987c193ad19e7a770a575a908cdba6740
# Parent  45986997f1fe9515d5f18c63496d2101a55c0aca
Deleted option_case_tac because exhaust_tac performs a similar function.

Deleted the duplicate proof of expand_option_case...

diff -r 45986997f1fe -r b3e39a2987c1 src/HOL/Option.ML
--- 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";