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. best, lucas -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
