src/HOL/Main.thy
changeset 14443 75910c7557c5
parent 14350 41b32020d0b3
child 14458 c2b96948730d
     1.1 --- a/src/HOL/Main.thy	Mon Mar 08 11:11:58 2004 +0100
     1.2 +++ b/src/HOL/Main.thy	Mon Mar 08 11:12:06 2004 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  header {* Main HOL *}
     1.6  
     1.7 -theory Main = Map + Hilbert_Choice + Extraction + Refute:
     1.8 +theory Main = Map + Infinite_Set + Extraction + Refute:
     1.9  
    1.10  text {*
    1.11    Theory @{text Main} includes everything.  Note that theory @{text