changeset 15131 | c69542757a4d |
parent 15063 | a43d771c18ac |
child 15140 | 322485b816ac |
--- a/src/HOL/Main.thy Mon Aug 16 14:21:54 2004 +0200 +++ b/src/HOL/Main.thy Mon Aug 16 14:22:27 2004 +0200 @@ -5,7 +5,9 @@ header {* Main HOL *} -theory Main = Map + Infinite_Set + Extraction + Refute: +theory Main +import Map Infinite_Set Extraction Refute +begin text {* Theory @{text Main} includes everything. Note that theory @{text