mb automata 2 Sections GenAutomata Doc

Def mk_imp(hyp, concl) == < hyp,concl >

is not mentioned in this or prior sections.

Try larger context: GenAutomata

mb automata 2 Sections GenAutomata Doc