--- a/doc-src/TutorialI/Rules/ROOT.ML Thu Oct 26 10:27:04 2000 +0200 +++ b/doc-src/TutorialI/Rules/ROOT.ML Thu Oct 26 11:27:48 2000 +0200 @@ -1,3 +1,4 @@ +(* ID: $Id$ *) use_thy "Basic"; use_thy "Blast"; use_thy "Force";