# HG changeset patch
# User wenzelm
# Date 1138559096 -3600
# Node ID 89b0fbbc4d8eb3f3427105e8a7e20435bfc56ec2
# Parent  6cbcfac5b72e1c32bdeb9d69a815db9faea1587e
tuned proof;

diff -r 6cbcfac5b72e -r 89b0fbbc4d8e src/HOLCF/Domain.thy
--- a/src/HOLCF/Domain.thy	Sun Jan 29 19:23:52 2006 +0100
+++ b/src/HOLCF/Domain.thy	Sun Jan 29 19:24:56 2006 +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 simp: norm_hhf_eq)
+by rule auto
 
 lemma exh_casedist3: "(P \<and> Q \<Longrightarrow> R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> R)"
 by rule auto