added an item about when the same quotient constant is defined twice (throws a bind exception in quoteint_def.ML)

no_document use_thys ["../Quot/QuotMain"];

use_thys ["Paper"];