--- a/doc-src/Functions/Thy/ROOT.ML Mon May 02 22:19:28 2011 +0200 +++ b/doc-src/Functions/Thy/ROOT.ML Mon May 02 22:31:46 2011 +0200 @@ -1,4 +1,1 @@ - -(* $Id$ *) - use_thy "Functions";