| changeset 18487 | 4d1015084876 |
| parent 17839 | 060dd0213f94 |
| child 18846 | 89b0fbbc4d8e |
--- 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