:: deftheorem defines pre-Meas MEASUR12:def 8 :
pre-Meas = OS_Meas | Family_of_Intervals;