src/HOL/Plain.thy
changeset 29304 5c71a6da989d
parent 27368 9f90ac19e32b
child 29609 a010aab5bed0
     1.1 --- a/src/HOL/Plain.thy	Thu Jan 01 23:31:59 2009 +0100
     1.2 +++ b/src/HOL/Plain.thy	Fri Jan 02 00:21:59 2009 +0100
     1.3 @@ -1,15 +1,14 @@
     1.4 -(*  Title:      HOL/Plain.thy
     1.5 -    ID:         $Id$
     1.6 -
     1.7 -Contains fundamental HOL tools and packages.  Does not include Hilbert_Choice.
     1.8 -*)
     1.9 -
    1.10  header {* Plain HOL *}
    1.11  
    1.12  theory Plain
    1.13  imports Datatype FunDef Record SAT Extraction
    1.14  begin
    1.15  
    1.16 +text {*
    1.17 +  Plain bootstrap of fundamental HOL tools and packages; does not
    1.18 +  include @{text Hilbert_Choice}.
    1.19 +*}
    1.20 +
    1.21  ML {* path_add "~~/src/HOL/Library" *}
    1.22  
    1.23  end