:: deftheorem defines SCM-VAL AMI_2:def 5 :
SCM-VAL = <%NAT,INT%>;