Re: [isabelle] Lemmas with multiple goals
> lemma "Goal1" and "Goal2"
> proof (rule X)
> show "Assumption"
> However, this does not work (it seems that only X(1) is applied).
Perhaps the Isar gurus have a better solution, but the best I could get is
lemma "Goal1" (is ?g1) and "Goal2" (is ?g2)
have "Assumption" sorry
thus ?g1 and ?g2 by (rule X)+
> BTW, since there is no ?thesis when multiple
> goals are present, is there a way of not retyping "Goal1" and "Goal2" in
> the second proof?
Yes, using the "is" syntax above.
I hope this helps. Have a nice day.
This archive was generated by a fusion of
Pipermail (Mailman edition) and