[isabelle] also and moreover



Hi,

I want to write a proof in this style:

lemma "XXX = ZZZ"
proof -
  have "XXX = AAA" sorry
  moreover
  have "ZZZ = BBB" sorry
  also have "... = AAA" sorry (* breaks here *)
  ultimately show ?thesis by simp
qed

Would it be possible for "moreover" to use a different calculation (?) to "also"?

If not, can the reason be put in S1.2 of isar-ref please?

cheers
peter

-- 
http://peteg.org/






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