changeset 14620 | 1be590fd2422 |
parent 14516 | a183dec876ab |
child 14652 | 5ddbdbadba06 |
--- 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";