# HG changeset patch
# User oheimb
# Date 905354622 -7200
# Node ID 3905974ad55514300f74817d6fb28943aae7c7b5
# Parent  ffc64812a70b3dc3fe02bd4f387a18d6421b6890
AddIffs[not_None_eq];
made wrapper ospec really safe

diff -r ffc64812a70b -r 3905974ad555 src/HOL/Option.ML
--- a/src/HOL/Option.ML	Wed Sep 09 17:21:33 1998 +0200
+++ b/src/HOL/Option.ML	Wed Sep 09 17:23:42 1998 +0200
@@ -9,6 +9,8 @@
 
 qed_goal "not_None_eq" thy "(x ~= None) = (? y. x = Some y)"
 	(K [induct_tac "x" 1, Auto_tac]);
+AddIffs[not_None_eq];
+
 
 section "case analysis in premises";
 
@@ -42,6 +44,7 @@
 Addsimps [the_Some];
 
 
+
 section "option_map";
 
 qed_goalw "option_map_None" thy [option_map_def] 
@@ -55,11 +58,14 @@
  (K [asm_full_simp_tac (simpset() addsplits [option.split]) 1]);
 AddIffs[option_map_eq_Some];
 
+
 section "o2s";
 
 qed_goal "ospec" thy 
 	"!!x. [| !x:o2s A. P x; A = Some x |] ==> P x" (K [Auto_tac]);
-claset_ref() := claset() addSaltern ("ospec", dtac ospec THEN' atac);
+claset_ref() := claset() addSaltern ("ospec", 
+				dmatch_tac [ospec] THEN' eq_assume_tac);
+
 
 val elem_o2s = prove_goal thy "!!X. x : o2s xo = (xo = Some x)"
  (K [optionE_tac "xo" 1, Auto_tac]);
diff -r ffc64812a70b -r 3905974ad555 src/HOL/Option.thy
--- a/src/HOL/Option.thy	Wed Sep 09 17:21:33 1998 +0200
+++ b/src/HOL/Option.thy	Wed Sep 09 17:23:42 1998 +0200
@@ -23,6 +23,7 @@
   o2s	   :: "'a option => 'a set"
 
 primrec
+
  "o2s  None    = {}"
  "o2s (Some x) = {x}"