src/HOL/Map.thy
changeset 66010 2f7d39285a1a
parent 63834 6a757f36997e
child 66583 ac183ddc9fef
     1.1 --- a/src/HOL/Map.thy	Mon Jun 05 20:03:01 2017 +0200
     1.2 +++ b/src/HOL/Map.thy	Mon Jun 05 15:59:41 2017 +0200
     1.3 @@ -485,7 +485,7 @@
     1.4  lemma domD: "a \<in> dom m \<Longrightarrow> \<exists>b. m a = Some b"
     1.5    by (cases "m a") (auto simp add: dom_def)
     1.6  
     1.7 -lemma domIff [iff, simp del]: "a \<in> dom m \<longleftrightarrow> m a \<noteq> None"
     1.8 +lemma domIff [iff, simp del, code_unfold]: "a \<in> dom m \<longleftrightarrow> m a \<noteq> None"
     1.9    by (simp add: dom_def)
    1.10  
    1.11  lemma dom_empty [simp]: "dom empty = {}"