:: deftheorem defines non_op ABCMIZ_1:def 8 :
non_op = 1;