src/HOL/Main.thy
changeset 13403 bc2b32ee62fd
parent 13367 ad307f0d80db
child 13755 a9bb54a3cfb7
     1.1 --- a/src/HOL/Main.thy	Sun Jul 21 15:37:04 2002 +0200
     1.2 +++ b/src/HOL/Main.thy	Sun Jul 21 15:42:30 2002 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  header {* Main HOL *}
     1.6  
     1.7 -theory Main = Map + Hilbert_Choice:
     1.8 +theory Main = Map + Hilbert_Choice + Extraction:
     1.9  
    1.10  text {*
    1.11    Theory @{text Main} includes everything.  Note that theory @{text