| changeset 14620 | 1be590fd2422 | 
| parent 14516 | a183dec876ab | 
| child 15647 | b1f486a9c56b | 
--- a/src/HOL/Import/Generate-HOL/ROOT.ML Sat Apr 17 20:04:23 2004 +0200 +++ b/src/HOL/Import/Generate-HOL/ROOT.ML Sat Apr 17 23:53:35 2004 +0200 @@ -1,3 +1,8 @@ +(* Title: HOL/Import/Generate-HOL/ROOT.ML + ID: $Id$ + Author: Sebastian Skalberg (TU Muenchen) +*) + with_path ".." use_thy "HOL4Compat"; with_path ".." use_thy "HOL4Syntax"; use_thy "GenHOL4Prob";