--- a/doc-src/Tutorial/Recdef/ROOT.ML Thu Jul 06 00:09:45 2000 +0200 +++ b/doc-src/Tutorial/Recdef/ROOT.ML Thu Jul 06 09:46:56 2000 +0200 @@ -1,5 +1,5 @@ use_thy "Examples"; -gcd.rules; +gcd.simps; use_thy "Sep1"; use_thy "Sep2"; (* test *)