diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/ROOT.ML --- a/Quot/ROOT.ML Thu Feb 11 09:23:59 2010 +0100 +++ b/Quot/ROOT.ML Thu Feb 11 10:06:02 2010 +0100 @@ -1,7 +1,7 @@ quick_and_dirty := true; no_document use_thys - ["QuotMain", + ["Quotient", "Examples/AbsRepTest", "Examples/FSet", "Examples/FSet2",