# HG changeset patch
# User huffman
# Date 1117834231 -7200
# Node ID 88ddef269510afcae9d88f721d18720489aad855
# Parent  422f836f6b3988e591a10c4be187e0c9d5c3ef7d
replaced cont with cont_def

diff -r 422f836f6b39 -r 88ddef269510 src/HOLCF/Discrete.thy
--- a/src/HOLCF/Discrete.thy	Fri Jun 03 23:29:48 2005 +0200
+++ b/src/HOLCF/Discrete.thy	Fri Jun 03 23:30:31 2005 +0200
@@ -68,7 +68,7 @@
 by (fast dest: discr_chain0 elim: arg_cong)
 
 lemma cont_discr [iff]: "cont(%x::('a::type)discr. f x)"
-apply (unfold cont is_lub_def is_ub_def)
+apply (unfold cont_def is_lub_def is_ub_def)
 apply (simp add: discr_chain_f_range0)
 done