[isabelle] Interleave in Isabelle



We noticed that the Isabelle Reference Manual from 1999 mentions an interleaving construct for tactics, which has disappeared in the manual from 2011. Is there a particular reason for this?

We ask because we are working on a paper on interleaving strategies for solving exercises (with the goal to follow and comment upon student interactions), and Isabelle seems to be the only prover that has offered interleave. We can imagine that efficiency might be a reason to exclude it: the number of possibilities increases (more than) exponentially in the length of the arguments when interleaving is used.

Any ideas?

Thanks,

Johan Jeuring






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.