# HG changeset patch
# User wenzelm
# Date 980366129 -3600
# Node ID 5b0d04078d2acc45a3d3daca7d840c695443edbe
# Parent  af160f8d3bd73470e684b895598afdf030f0e4cd
empty_upd_none;

diff -r af160f8d3bd7 -r 5b0d04078d2a src/HOL/Map.ML
--- a/src/HOL/Map.ML	Wed Jan 24 17:53:01 2001 +0100
+++ b/src/HOL/Map.ML	Wed Jan 24 20:55:29 2001 +0100
@@ -3,7 +3,7 @@
     Author:     Tobias Nipkow
     Copyright   1997 TU Muenchen
 
-Map lemmas
+Map lemmas.
 *)
 
 section "empty";
@@ -13,6 +13,12 @@
 qed "empty_def2";
 Addsimps [empty_def2];
 
+Goal "empty(x := None) = empty";
+by (rtac ext 1);
+by (Simp_tac 1);
+qed "empty_upd_none";
+Addsimps [empty_upd_none];
+
 Goal "sum_case empty empty = empty";
 by (rtac ext 1);
 by (simp_tac (simpset() addsplits [sum.split]) 1);
@@ -202,8 +208,8 @@
 
 Goalw [dom_def] "finite (dom (map_of l))";
 by (induct_tac "l" 1);
-by (auto_tac (claset(), 
-	      simpset() addsimps [insert_Collect RS sym]));
+by (auto_tac (claset(),
+              simpset() addsimps [insert_Collect RS sym]));
 qed "finite_dom_map_of";
 
 Goalw [dom_def] "dom(m++n) = dom n Un dom m";