include "LIN/joint_LTL_LIN_semantics_paolo.ma". include "LIN/LIN_paolo.ma". (* CSC: syntax.ma in RTLabs *) definition LIN_semantics : sem_params ≝ make_sem_lin_params LIN (LTL_LIN_semantics ?).