| changeset 15131 | c69542757a4d |
| parent 15045 | d59f7e2e18d3 |
| child 15140 | 322485b816ac |
--- a/src/HOL/Infinite_Set.thy Mon Aug 16 14:21:54 2004 +0200 +++ b/src/HOL/Infinite_Set.thy Mon Aug 16 14:22:27 2004 +0200 @@ -5,7 +5,9 @@ header {* Infnite Sets and Related Concepts*} -theory Infinite_Set = Hilbert_Choice + Finite_Set + SetInterval: +theory Infinite_Set +import Hilbert_Choice Finite_Set SetInterval +begin subsection "Infinite Sets"