# HG changeset patch
# User oheimb
# Date 950901880 -3600
# Node ID a8d2606f49218eb37bb92bdb1afa2baf03d7a169
# Parent  666d3a4f3b9dcee3fd4a2fddfae5ec75787d23c9
added domI, domD

diff -r 666d3a4f3b9d -r a8d2606f4921 src/HOL/IMPP/Com.ML
--- 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)";
diff -r 666d3a4f3b9d -r a8d2606f4921 src/HOL/Map.ML
--- 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";