[isabelle-dev] Interrupt exception

[Lucas Dixon]

Florian Haftmann wrote:
> Hi Lucas,
> 
>>   apply (unfold Product_Type.pair_collapse[symmetric, of "al"])
> 
> The equation Product_Type.pair_collapse[symmetric, of "al"] can be
> unfolded forever, so the method invocation does not terminate, leading
> to an unspecified behaviour of the system!
> 
> As a quick replacement, consider
> 
> 	apply (subst ...)
> 
> In the end it is better to write a structured Isar proof text which
> allows fine granular control over delicate steps.

Thanks, I know this - I wrote subst :)

The point was just that unfold should probably be giving an error 
message of some more readable sort.

best,
lucas

-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.