# HG changeset patch
# User oheimb
# Date 895156353 -7200
# Node ID 0fd0b3f3bc250167e2990fe79f815bf7b83b32a1
# Parent  53900a320a87e7611679f0941eb7d7d17b2cc9d1
added option_map_o_update

diff -r 53900a320a87 -r 0fd0b3f3bc25 src/HOL/Map.ML
--- a/src/HOL/Map.ML	Wed May 13 19:06:57 1998 +0200
+++ b/src/HOL/Map.ML	Thu May 14 16:32:33 1998 +0200
@@ -24,6 +24,9 @@
 	(K [rtac ext 1, Asm_simp_tac 1]);
 (*Addsimps [update_same, update_other, update_triv];*)
 
+qed_goal "option_map_o_update" thy 
+	"option_map f o m[a|->b] = (option_map f o m)[a|->f b]" 
+	(K [rtac ext 1,Auto_tac]);
 
 section "++";
 
@@ -45,7 +48,7 @@
 by (simp_tac (simpset() addsplits [split_option_case]) 1);
 qed_spec_mp "override_Some_iff";
 
-bind_thm("override_SomeD", standard(override_Some_iff RS iffD1));
+bind_thm ("override_SomeD", standard(override_Some_iff RS iffD1));
 
 goalw thy [override_def]
  "((m ++ n) k = None) = (n k = None & m k = None)";