src/HOL/BNF_Examples/Koenig.thy
changeset 57634 efc00b9b8680
parent 57207 df0f8ad7cc30
equal deleted inserted replaced
57633:4ff8c090d580 57634:efc00b9b8680
     4     Copyright   2012
     4     Copyright   2012
     5 
     5 
     6 Koenig's lemma.
     6 Koenig's lemma.
     7 *)
     7 *)
     8 
     8 
     9 header {* Koenig's lemma *}
     9 header {* Koenig's Lemma *}
    10 
    10 
    11 theory Koenig
    11 theory Koenig
    12 imports TreeFI Stream
    12 imports TreeFI Stream
    13 begin
    13 begin
    14 
    14