That was due to my reforms of the sublist/subseq stuff and should be
repaired by this afternoon. Tomorrow's slow tests should run through
fine again. Unfortunately, these slow sessions don't have the same rapid
testing cycle as the normal sessions.
Manuel
On 2017-06-01 16:19, Florian
isabelle: 3bec939bd808 tip
afp: 09eedef13195 tip
> *** {n. enat n < llength stls \
> *** (case lnth stls n of
> ***(s, tl, s') \ \ \move s tl s')} ::
> *** nat set
> ***
> *** Coercion Inference:
> ***
> *** Local coercion insertion on the operand failed:
> *** Cannot generate
