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.
tuned proof;
authorwenzelm
Sun, 29 Jan 2006 19:24:56 +0100
changeset 18846 89b0fbbc4d8e
parent 18845 6cbcfac5b72e
child 18847 5fac129ae936
tuned proof;
src/HOLCF/Domain.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle