Re: [isabelle] Cannot solve all subgoals
Thank you and also Lars Hupel for your answers. This list is indeed
I was using show statements with ==> mostly because I had lots of them
from unfolding a locale and most of them were rather trivial one-line
proofs. So I was looking for a way to avoid Isar style verbose proofs
in this specific case without resorting to apply scripts.
On 07/02/2015 04:10 PM, Lars Noschinski wrote:
> On 02.07.2015 15:58, Christoph Dittmann wrote:
>> sometimes when I prove a lemma with multiple subgoals one after the
>> other, the number of subgoals does not shrink and in the end there are
>> unsolved subgoals that I don't understand.
> The short answer is: Don't use "_ ==> _" in show statements. For a
> longer explanation, see the following answer on Stackoverflow:
> -- Lars
This archive was generated by a fusion of
Pipermail (Mailman edition) and