| 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";