1.1 --- a/src/HOLCF/Domain.thy	Thu Dec 22 00:29:20 2005 +0100
     1.2 +++ b/src/HOLCF/Domain.thy	Thu Dec 22 00:29:22 2005 +0100
     1.3 @@ -191,7 +191,7 @@
     1.4  by rule auto
     1.5  
     1.6  lemma exh_casedist2: "(\<exists>x. P x \<Longrightarrow> Q) \<equiv> (\<And>x. P x \<Longrightarrow> Q)"
     1.7 -by rule auto
     1.8 +by rule (auto simp: norm_hhf_eq)
     1.9  
    1.10  lemma exh_casedist3: "(P \<and> Q \<Longrightarrow> R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> R)"
    1.11  by rule auto