[isabelle-dev] Interrupt exception

Lucas Dixon ldixon at inf.ed.ac.uk
Wed Jul 15 12:46:09 CEST 2009

Makarius wrote:
> 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?

Yes, I'm sure you are right; I'm using Isabelle (1d4d0b305f16: date: 
     Fri Jul 10 09:24:50 2009 +0200), and PolyML (svn 801, 2009-07-12)

The problem came up when I was writing a tactic and I wanted to unfold 
all occurences within a goal but not do this recursively - I wanted any 
introduced occurrences to be untouched. I was simulating this within a 
tactic script as an experiment. But perhaps the idea of unfold all 
current occurrences (modulo critical pairs) would be a sensible 
semantics for unfold? It seems like a sensible semantics for something, 
call it unfold or something else :)


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

More information about the isabelle-dev mailing list