Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
exh_casedist2: norm_hhf_eq;
authorwenzelm
Thu, 22 Dec 2005 00:29:22 +0100
changeset 18487 4d1015084876
parent 18486 bf8637d9d53b
child 18488 a353a61c4544
exh_casedist2: norm_hhf_eq;
src/HOLCF/Domain.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle