- Inserted additional check for equality types in check_mode_clause that
avoids ill-typed code to be generated.
- Mode inference algorithm now outputs additional diagnostic messages.
Goal "!xs. linInfixList t xs = infixList t @ xs";
by(induct_tac "t" 1);
by(Simp_tac 1);
by(Asm_simp_tac 1);