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".
This archive was generated by a fusion of
Pipermail (Mailman edition) and