src/HOL/Import/HOL/ROOT.ML
changeset 14620 1be590fd2422
parent 14516 a183dec876ab
child 14652 5ddbdbadba06
     1.1 --- a/src/HOL/Import/HOL/ROOT.ML	Sat Apr 17 20:04:23 2004 +0200
     1.2 +++ b/src/HOL/Import/HOL/ROOT.ML	Sat Apr 17 23:53:35 2004 +0200
     1.3 @@ -1,3 +1,8 @@
     1.4 +(*  Title:      HOL/Import/HOL/ROOT.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Sebastian Skalberg (TU Muenchen)
     1.7 +*)
     1.8 +
     1.9  with_path ".." use_thy "HOL4Compat";
    1.10  with_path ".." use_thy "HOL4Syntax";
    1.11  setmp quick_and_dirty true use_thy "HOL4Prob";