added domI, domD

--- a/src/HOL/IMPP/Com.ML	Fri Feb 18 20:24:16 2000 +0100
+++ b/src/HOL/IMPP/Com.ML	Fri Feb 18 20:24:40 2000 +0100
@@ -1,12 +1,3 @@
-Goalw [dom_def] "m a = Some b ==> a : dom m";
-by Auto_tac;
-qed "domI";
-
-Goalw [dom_def] "a : dom m ==> ? b. m a = Some b";
-by Auto_tac;
-qed "domD";
-AddSDs [domD];
-
 val make_imp_tac = EVERY'[rtac mp, fn i => atac (i+1), etac thin_rl];
 
 Goalw [body_def] "finite (dom body)";

--- a/src/HOL/Map.ML	Fri Feb 18 20:24:16 2000 +0100
+++ b/src/HOL/Map.ML	Fri Feb 18 20:24:40 2000 +0100
@@ -148,6 +148,15 @@
 
 section "dom";
 
+Goalw [dom_def] "m a = Some b ==> a : dom m";
+by Auto_tac;
+qed "domI";
+
+Goalw [dom_def] "a : dom m ==> ? b. m a = Some b";
+by Auto_tac;
+qed "domD";
+AddSDs [domD];
+
 Goalw [dom_def] "dom empty = {}";
 by (Simp_tac 1);
 qed "dom_empty";