src/HOL/Library/Countable_Set.thy
changeset 58881 b9556a055632
parent 57234 596a499318ab
child 60058 f17bb06599f6
equal deleted inserted replaced
58880:0baae4311a9f 58881:b9556a055632
     1 (*  Title:      HOL/Library/Countable_Set.thy
     1 (*  Title:      HOL/Library/Countable_Set.thy
     2     Author:     Johannes Hölzl
     2     Author:     Johannes Hölzl
     3     Author:     Andrei Popescu
     3     Author:     Andrei Popescu
     4 *)
     4 *)
     5 
     5 
     6 header {* Countable sets *}
     6 section {* Countable sets *}
     7 
     7 
     8 theory Countable_Set
     8 theory Countable_Set
     9 imports Countable Infinite_Set
     9 imports Countable Infinite_Set
    10 begin
    10 begin
    11 
    11