Quot/QuotMain.thy
2010-01-16 Christian Urban 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
less more (0) -30 -10 -1 tip