Re: [isabelle] Cannot solve all subgoals



On 02.07.2015 16:54, Christoph Dittmann wrote:
> 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.

When they are really trivial, you might also be able to solve them by
giving a single proof method to the closing "qed".

  -- Lars




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