[isabelle-dev] Interrupt exception
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