diff -r 8876ad83b1fb -r 1be590fd2422 src/HOL/Import/HOL/ROOT.ML --- a/src/HOL/Import/HOL/ROOT.ML Sat Apr 17 20:04:23 2004 +0200 +++ b/src/HOL/Import/HOL/ROOT.ML Sat Apr 17 23:53:35 2004 +0200 @@ -1,3 +1,8 @@ +(* Title: HOL/Import/HOL/ROOT.ML + ID: $Id$ + Author: Sebastian Skalberg (TU Muenchen) +*) + with_path ".." use_thy "HOL4Compat"; with_path ".." use_thy "HOL4Syntax"; setmp quick_and_dirty true use_thy "HOL4Prob";