src/HOL/Map.ML
changeset 13811 f39f67982854
parent 11015 55d95834c815
child 13890 90611b4e0054
--- a/src/HOL/Map.ML	Fri Feb 07 16:40:23 2003 +0100
+++ b/src/HOL/Map.ML	Sat Feb 08 14:46:22 2003 +0100
@@ -221,7 +221,12 @@
 Goalw [dom_def] "a : dom m ==> ? b. m a = Some b";
 by Auto_tac;
 qed "domD";
-AddSDs [domD];
+
+Goalw [dom_def] "(a : dom m) = (m a ~= None)";
+by Auto_tac;
+qed "domIff";
+AddIffs [domIff];
+Delsimps [domIff];
 
 Goalw [dom_def] "dom empty = {}";
 by (Simp_tac 1);