doc-src/TutorialI/Sets/ROOT.ML
changeset 10341 6eb91805a012
parent 10294 2ec9c808a8a7
child 42637 381fdcab0f36
--- a/doc-src/TutorialI/Sets/ROOT.ML	Thu Oct 26 10:27:04 2000 +0200
+++ b/doc-src/TutorialI/Sets/ROOT.ML	Thu Oct 26 11:27:48 2000 +0200
@@ -1,3 +1,4 @@
+(* ID:         $Id$ *)
 use_thy "Examples";
 use_thy "Functions";
 use_thy "Relations";