src/HOL/Main.thy
changeset 15131 c69542757a4d
parent 15063 a43d771c18ac
child 15140 322485b816ac
equal deleted inserted replaced
15130:dc6be28d7f4e 15131:c69542757a4d
     3     Author:     Stefan Berghofer, Tobias Nipkow, Tjark Weber, Markus Wenzel (TU Muenchen)
     3     Author:     Stefan Berghofer, Tobias Nipkow, Tjark Weber, Markus Wenzel (TU Muenchen)
     4 *)
     4 *)
     5 
     5 
     6 header {* Main HOL *}
     6 header {* Main HOL *}
     7 
     7 
     8 theory Main = Map + Infinite_Set + Extraction + Refute:
     8 theory Main
       
     9 import Map Infinite_Set Extraction Refute
       
    10 begin
     9 
    11 
    10 text {*
    12 text {*
    11   Theory @{text Main} includes everything.  Note that theory @{text
    13   Theory @{text Main} includes everything.  Note that theory @{text
    12   PreList} already includes most HOL theories.
    14   PreList} already includes most HOL theories.
    13 *}
    15 *}