# HG changeset patch
# User oheimb
# Date 906411997 -7200
# Node ID e2484f1786b7cb6e278a20b587e181ae889161ab
# Parent  54e313ed22baa9ef16f44a52b77e6193fbdf71f2
added addD2, addE2, addSD2, and addSE2
added not_Some_eq, also to simpset() and claset()

diff -r 54e313ed22ba -r e2484f1786b7 src/HOL/Option.ML
--- a/src/HOL/Option.ML	Mon Sep 21 23:04:51 1998 +0200
+++ b/src/HOL/Option.ML	Mon Sep 21 23:06:37 1998 +0200
@@ -11,6 +11,10 @@
 	(K [induct_tac "x" 1, Auto_tac]);
 AddIffs[not_None_eq];
 
+qed_goal "not_Some_eq" thy "(!y. x ~= Some y) = (x = None)"
+	(K [induct_tac "x" 1, Auto_tac]);
+AddIffs[not_Some_eq];
+
 
 section "case analysis in premises";
 
@@ -63,8 +67,8 @@
 
 qed_goal "ospec" thy 
 	"!!x. [| !x:o2s A. P x; A = Some x |] ==> P x" (K [Auto_tac]);
-claset_ref() := claset() addSaltern ("ospec", 
-				dmatch_tac [ospec] THEN' eq_assume_tac);
+AddDs[ospec];
+claset_ref() := claset() addSD2 ("ospec", ospec);
 
 
 val elem_o2s = prove_goal thy "!!X. x : o2s xo = (xo = Some x)"