src/HOL/Infinite_Set.thy
changeset 19457 b6eb4b4546fa
parent 19363 667b5ea637dd
child 19537 213ff8b0c60c
equal deleted inserted replaced
19456:b5bfd2d17dd3 19457:b6eb4b4546fa
     1 (*  Title:      HOL/Infnite_Set.thy
     1 (*  Title:      HOL/Infnite_Set.thy
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Stephan Merz 
     3     Author:     Stephan Merz 
     4 *)
     4 *)
     5 
     5 
     6 header {* Infnite Sets and Related Concepts*}
     6 header {* Infinite Sets and Related Concepts*}
     7 
     7 
     8 theory Infinite_Set
     8 theory Infinite_Set
     9 imports Hilbert_Choice Binomial
     9 imports Hilbert_Choice Binomial
    10 begin
    10 begin
    11 
    11