# HG changeset patch
# User huffman
# Date 1272991289 25200
# Node ID e37b4338c71fa2f0d615ba02380fbe0a163ad37f
# Parent  f376af79f6b7c1cabbbe0de27695355f90c3f0e5
declare cont_discrete_cpo [cont2cont]

diff -r f376af79f6b7 -r e37b4338c71f src/HOLCF/Cont.thy
--- 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)