is mentioned by

Def st_app1(s1;s2) == Case(s1) Case a;b = > if st_eq(a;s2) < b > else < > fi Default = > < >

[st_app1]

In prior sections: bool 1 mb nat mb events mb list 2 mb automata 1 int 2 list 1 prog 1 num thy 1 mb list 1 mb declaration

Try larger context: GenAutomata