# HG changeset patch
# User oheimb
# Date 963584936 -7200
# Node ID d66f25a206b4fcd605dbe8481da49012808b31df
# Parent  40bab6613000ba2f75b6a79ef35254bb2216270e
added sum_case_empty_empty (also to simpset)

diff -r 40bab6613000 -r d66f25a206b4 src/HOL/Map.ML
--- a/src/HOL/Map.ML	Fri Jul 14 16:28:49 2000 +0200
+++ b/src/HOL/Map.ML	Fri Jul 14 16:28:56 2000 +0200
@@ -13,6 +13,12 @@
 qed "empty_def2";
 Addsimps [empty_def2];
 
+Goal "sum_case empty empty = empty";
+by (rtac ext 1);
+by (simp_tac (simpset() addsplits [sum.split]) 1);
+qed "sum_case_empty_empty";
+Addsimps [sum_case_empty_empty];
+
 
 section "map_upd";