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.
declare cont_discrete_cpo [cont2cont]
authorhuffman
Tue, 04 May 2010 09:41:29 -0700
changeset 36658 e37b4338c71f
parent 36657 f376af79f6b7
child 36659 f794e92784aa
declare cont_discrete_cpo [cont2cont]
src/HOLCF/Cont.thy file | annotate | diff | comparison | revisions 
--- a/src/HOLCF/Cont.thy	Mon May 03 20:42:58 2010 -0700
+++ b/src/HOLCF/Cont.thy	Tue May 04 09:41:29 2010 -0700
@@ -237,7 +237,7 @@
 
 text {* functions with discrete domain *}
 
-lemma cont_discrete_cpo [simp]: "cont (f::'a::discrete_cpo \<Rightarrow> 'b::cpo)"
+lemma cont_discrete_cpo [cont2cont]: "cont (f::'a::discrete_cpo \<Rightarrow> 'b::cpo)"
 apply (rule contI)
 apply (drule discrete_chain_const, clarify)
 apply (simp add: lub_const)
isabelle