src/HOL/Map.ML
changeset 9342 d66f25a206b4
parent 9018 b16bc0b5ad21
child 9356 30c3d3e308ee
--- 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";