# HG changeset patch
# User wenzelm
# Date 1135207762 -3600
# Node ID 4d10150848760dcd52e63e626565ca0c3227dfdb
# Parent  bf8637d9d53b7a023ae4ea320b93a1b2dd1ef39d
exh_casedist2: norm_hhf_eq;

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