diff -r bf8637d9d53b -r 4d1015084876 src/HOLCF/Domain.thy
--- a/src/HOLCF/Domain.thy	Thu Dec 22 00:29:20 2005 +0100
+++ b/src/HOLCF/Domain.thy	Thu Dec 22 00:29:22 2005 +0100
@@ -191,7 +191,7 @@
 by rule auto
 
 lemma exh_casedist2: "(\<exists>x. P x \<Longrightarrow> Q) \<equiv> (\<And>x. P x \<Longrightarrow> Q)"
-by rule auto
+by rule (auto simp: norm_hhf_eq)
 
 lemma exh_casedist3: "(P \<and> Q \<Longrightarrow> R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> R)"
 by rule auto