1open HolKernel Parse boolLib testutils
2
3val _ = List.app convtest [
4  ("bagSimps.CANCEL_CONV(1)", bagSimps.CANCEL_CONV,
5   ���b5 + (b1: 'a bag) + b2 + b4 - (b2 + b1)���,
6   ���(b4:'a bag) + b5 - {||}���),
7  ("bagSimps.CANCEL_CONV(2)", bagSimps.CANCEL_CONV,
8   ���b5 + (b1: 'a bag) + b2 + b4 = b2 + b6 + b1���, ���(b4:'a bag) + b5 = b6���),
9  ("bagSimps.CANCEL_CONV(3)", bagSimps.CANCEL_CONV,
10   ���SUB_BAG b2 (b5 + (b1: 'a bag) + b2 + b4)���, ���{||} <= b1 + b4 + b5���)
11];
12