# HG changeset patch
# User oheimb
# Date 963584938 -7200
# Node ID 1c47549389806b2237175b9e5a73519c324ca0e7
# Parent  d66f25a206b4fcd605dbe8481da49012808b31df
added option_map_o_sum_case (also to simpset)

diff -r d66f25a206b4 -r 1c4754938980 src/HOL/Option.ML
--- a/src/HOL/Option.ML	Fri Jul 14 16:28:56 2000 +0200
+++ b/src/HOL/Option.ML	Fri Jul 14 16:28:58 2000 +0200
@@ -60,6 +60,13 @@
 qed "option_map_eq_Some";
 AddIffs[option_map_eq_Some];
 
+Goal 
+"option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)";
+by (rtac ext 1);
+by (simp_tac (simpset() addsplits [sum.split]) 1);
+qed "option_map_o_sum_case";
+Addsimps [option_map_o_sum_case];
+
 
 section "o2s";