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 <sven.schneider.pub at gmx.de> 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.