:: deftheorem defines InsCodes COMPOS_0:def 2 :
for S being standard-ins set holds InsCodes S = proj1_3 S;