signature INFIX_CONV =+− sig+− val then_conv : Thm.conv * Thm.conv -> Thm.conv+− val else_conv : Thm.conv * Thm.conv -> Thm.conv+− end+− +− structure InfixConv : INFIX_CONV = Conv+− +− open InfixConv+−