[isabelle-dev] Interrupt exception

[Florian Haftmann]

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.

Hope this helps,
	Florian

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 252 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20090713/953ab242/attachment.sig>