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