replaced cont with cont_def
authorhuffman
Fri Jun 03 23:30:31 2005 +0200 (2005-06-03)
changeset 1621388ddef269510
parent 16212 422f836f6b39
child 16214 e3816a7db016
replaced cont with cont_def
src/HOLCF/Discrete.thy
     1.1 --- a/src/HOLCF/Discrete.thy	Fri Jun 03 23:29:48 2005 +0200
     1.2 +++ b/src/HOLCF/Discrete.thy	Fri Jun 03 23:30:31 2005 +0200
     1.3 @@ -68,7 +68,7 @@
     1.4  by (fast dest: discr_chain0 elim: arg_cong)
     1.5  
     1.6  lemma cont_discr [iff]: "cont(%x::('a::type)discr. f x)"
     1.7 -apply (unfold cont is_lub_def is_ub_def)
     1.8 +apply (unfold cont_def is_lub_def is_ub_def)
     1.9  apply (simp add: discr_chain_f_range0)
    1.10  done
    1.11