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.

Christoph

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:
> 
> http://stackoverflow.com/questions/25285797/taming-meta-implication-in-isar-proofs/25442787#25442787
> 
>   -- Lars
> 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.