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://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20090713/953ab242/attachment.pgp>
