src/HOL/HOLCF/FOCUS/Stream_adm.thy
changeset 43919 a7e4fb1a0502
parent 42151 4da4fc77664b
child 43921 e8511be08ddd
     1.1 --- a/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Tue Jul 19 11:15:38 2011 +0200
     1.2 +++ b/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Tue Jul 19 14:35:44 2011 +0200
     1.3 @@ -74,7 +74,7 @@
     1.4  apply (   erule spec)
     1.5  apply (  assumption)
     1.6  apply ( assumption)
     1.7 -apply (metis inat_ord_code(4) slen_infinite)
     1.8 +apply (metis enat_ord_code(4) slen_infinite)
     1.9  done
    1.10  
    1.11  (* should be without reference to stream length? *)