adjusted dom rules

--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Fri Feb 07 16:40:23 2003 +0100
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Sat Feb 08 14:46:22 2003 +0100
@@ -2247,7 +2247,7 @@
 proof -
   -- {* To properly perform induction on the evaluation relation we have to
         generalize the lemma to terms not only expressions. *}
-  {fix t val
+  { fix t val
    assume eval': "prg Env\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (val,s1)"  
    assume bool': "Env\<turnstile> t\<Colon>Inl (PrimT Boolean)"
    assume expr:  "\<exists> expr. t=In1l expr"
@@ -3634,7 +3634,7 @@
         hence "normal s2"
           by (cases s2) simp
         with nrmAss_A' nrm_A_A' s2_s3 show ?thesis
-          by auto
+          by blast
       qed
     qed
     moreover

--- 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);