explicit handling of mem_def, avoiding the use of the simplifier; this fixes some quotient_type definitions

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

use_thys ["Paper"];