is mentioned by

Def i:I M(i) == mk_sm(M(i).da for i I, M(i).ds for i I, s.i:I. M(i).init(s), s1,a,s2. i:I. M(i).trans(s1,a,s2))

[sm_all]

In prior sections: mb declaration mb record

Try larger context: GenAutomata