src/HOL/HOLCF/FOCUS/Stream_adm.thy
changeset 43921 e8511be08ddd
parent 43919 a7e4fb1a0502
child 43924 1165fe965da8
     1.1 --- a/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Tue Jul 19 14:36:12 2011 +0200
     1.2 +++ b/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Tue Jul 19 14:37:09 2011 +0200
     1.3 @@ -87,7 +87,7 @@
     1.4  done
     1.5  
     1.6  
     1.7 -(* context (theory "Nat_InFinity");*)
     1.8 +(* context (theory "Extended_Nat");*)
     1.9  lemma ile_lemma: "Fin (i + j) <= x ==> Fin i <= x"
    1.10    by (rule order_trans) auto
    1.11