[isabelle-dev] Interrupt exception

Lucas Dixon ldixon at inf.ed.ac.uk
Wed Jul 15 01:02:44 CEST 2009

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.


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

More information about the isabelle-dev mailing list