mb structures Sections GenAutomata Doc

Def i=j == if i=j true ; false fi

is mentioned by

Def =(M)(m_1,m_2) == ((content(M)(m_1)) =(cEQ(M)) (content(M)(m_2)))sender(M)(m_1) = sender(M)(m_2) (uid(M)(m_1)=uid(M)(m_2))[msg_eq]

In prior sections: bool 1 sqequal 1 prog 1 mb nat int 2 mb basic num thy 1

Try larger context: GenAutomata

mb structures Sections GenAutomata Doc