Re: [isabelle] Cannot solve all subgoals

Thank you and also Lars Hupel for your answers.  This list is indeed
very helpful!

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:
>> Hi,
>> 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 MHonArc.