liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals

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

use_thys ["Paper"];