src/HOL/HOLCF/FOCUS/Fstreams.thy
changeset 43921 e8511be08ddd
parent 43919 a7e4fb1a0502
child 43924 1165fe965da8
     1.1 --- a/src/HOL/HOLCF/FOCUS/Fstreams.thy	Tue Jul 19 14:36:12 2011 +0200
     1.2 +++ b/src/HOL/HOLCF/FOCUS/Fstreams.thy	Tue Jul 19 14:37:09 2011 +0200
     1.3 @@ -99,7 +99,7 @@
     1.4  lemma last_UU[simp]:"last UU = undefined"
     1.5  by (simp add: last_def jth_def enat_defs)
     1.6  
     1.7 -lemma last_infinite[simp]:"#s = Infty ==> last s = undefined"
     1.8 +lemma last_infinite[simp]:"#s = \<infinity> ==> last s = undefined"
     1.9  by (simp add: last_def)
    1.10  
    1.11  lemma jth_slen_lemma1:"n <= k & Fin n = #s ==> jth k s = undefined"