# HG changeset patch
# User oheimb
# Date 893698159 -7200
# Node ID fc5773ae27902600552ef1471244ca305cc8d46d
# Parent  f90a427d903f36578aac56f0fdb22c1eb47d462b
added option_map_eq_Some via AddIffs

diff -r f90a427d903f -r fc5773ae2790 src/HOL/Option.ML
--- a/src/HOL/Option.ML	Mon Apr 27 18:06:22 1998 +0200
+++ b/src/HOL/Option.ML	Mon Apr 27 19:29:19 1998 +0200
@@ -56,8 +56,7 @@
 val option_map_eq_Some = prove_goalw thy [option_map_def]
 	"(option_map f xo = Some y) = (? z. xo = Some z & f z = y)" 
  (K [asm_full_simp_tac (simpset() addsplits [split_option_case]) 1]);
-AddSDs[option_map_eq_Some RS iffD1];
-Addsimps [option_map_eq_Some];
+AddIffs[option_map_eq_Some];
 
 section "o2s";