Re: [isabelle] Cannot solve all subgoals

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.