induction_int_lex : new induction tactic (labels only, no heuristic provided) for ordered int tuples.

this is an experimental feature, not yet proved, not yet tested.
Currently, it is only used when a debug flag "implicit_post" is set.
It might need some tweaking to work well with booleans.

induction tactic: cleaning up (an old version of tactic (induction_ty) is removed). Induction on integers will be fixed soon (actually does not work)

illustrates the new typing system of WhyML
with a mutable field containing a mutable data structure