src/HOL/Main.thy
changeset 15140 322485b816ac
parent 15131 c69542757a4d
child 15151 429666b09783
equal deleted inserted replaced
15139:58cd3404cf75 15140:322485b816ac
     4 *)
     4 *)
     5 
     5 
     6 header {* Main HOL *}
     6 header {* Main HOL *}
     7 
     7 
     8 theory Main
     8 theory Main
     9 import Map Infinite_Set Extraction Refute
     9 imports Map Infinite_Set Extraction Refute
    10 begin
    10 begin
    11 
    11 
    12 text {*
    12 text {*
    13   Theory @{text Main} includes everything.  Note that theory @{text
    13   Theory @{text Main} includes everything.  Note that theory @{text
    14   PreList} already includes most HOL theories.
    14   PreList} already includes most HOL theories.