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:

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.