Re: [isabelle] Transfer Isabelle2011 Code to Isabelle2014

The “back” command is intended to allow interactive exploration of the multiple results delivered by a proof method. But leaving instances of this command in a proof script makes it unusually difficult to read and fragile. You can fix this problem in a number of ways, for example by explicitly instantiating variables in a theorem or by combining a series of proof methods where the last one will fail unless the last choice was made earlier, a bit like constraint satisfaction in Prolog.

Larry Paulson

> On 20 Feb 2015, at 15:21, Sven Schneider < at> wrote:
> This is what I also believed.
> Why is it not required that back always produces an immediate fault,
> i.e., always a unique result?
> Without 'back' the first result is chosen but if the order changes, this
> first element may be a different than before.

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