[isabelle-dev] Interrupt exception
makarius at sketis.net
Wed Jul 15 10:48:51 CEST 2009
On Wed, 15 Jul 2009, Lucas Dixon wrote:
>>> 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!
> The point was just that unfold should probably be giving an error message of
> some more readable sort.
The interrupt exception is probably produced by the Poly/ML runtime system
when it runs out of resources. The behaviour might have changed a bit in
recent internal versions. Which one did you use?
More information about the isabelle-dev