# HG changeset patch
# User oheimb
# Date 964194394 -7200
# Node ID d3109d5173071950583a3bb755b88c4079912140
# Parent  effc8d44c89c763910e7d5846fb458c164dbd2ea
added map_upd_nonempty, also to simpset

diff -r effc8d44c89c -r d3109d517307 src/HOL/Map.ML
--- a/src/HOL/Map.ML	Fri Jul 21 17:46:29 2000 +0200
+++ b/src/HOL/Map.ML	Fri Jul 21 17:46:34 2000 +0200
@@ -27,6 +27,13 @@
 by (Asm_simp_tac 1);
 qed "map_upd_triv";
 
+Goal "t(k|->x) ~= empty";
+by Safe_tac;
+by (dres_inst_tac [("x","k")] fun_cong 1);
+by (Full_simp_tac 1);
+qed "map_upd_nonempty";
+Addsimps[map_upd_nonempty];
+
 Goalw [image_def] "finite (range f) ==> finite (range (f(a|->b)))";
 by (full_simp_tac (simpset() addsimps [full_SetCompr_eq]) 1);
 by (rtac finite_subset 1);