Hello, I encountered a proof in which the processing of "show ?thesis" would not terminate, displaying many "Unification bound exceeded" messages. I reduced it to the following example, where the processing of "show "P"" does not terminate. Could anyone explain this behavior? Is it possible to reliably avoid it? Removing the type annotation ::"'a â 'a â 'a" in the "fix" line resolves the problem. However, I don't understand why. I'm using Isabelle 2015. Thanks, Giuliano theory Test imports Main begin notepad begin have "â Q (f::'a â 'a â 'a) P . (âs. Q (f s)) â P" proof - fix Q and f::"'a â 'a â 'a" and P assume "â s . Q (f s)" show "P"
Description: OpenPGP digital signature