diff -r 41dff1b862bf -r 381fdcab0f36 doc-src/TutorialI/Sets/ROOT.ML --- a/doc-src/TutorialI/Sets/ROOT.ML Mon May 02 22:19:28 2011 +0200 +++ b/doc-src/TutorialI/Sets/ROOT.ML Mon May 02 22:31:46 2011 +0200 @@ -1,4 +1,3 @@ -(* ID: $Id$ *) use_thy "Examples"; use_thy "Functions"; use_thy "Relations";