:: deftheorem defines REAL_Music MUSIC_S1:def 7 :
REAL_Music = MusicStruct(# REALPLUS,EQUIV_REAL_ratio,REAL_ratio #);