Re: [isabelle] also and moreover
Just a comment: it seems to work out ok if I put the have-also-finally bit inside curly braces...
lemma "XXX = ZZZ"
have "XXX = AAA" sorry
have "ZZZ = BBB" sorry
also have "... = AAA" sorry
finally have "ZZZ = AAA" sorry (* line added *)
ultimately show ?thesis by simp
On 8 Mar 2012, at 03:10, Peter Gammie wrote:
> I want to write a proof in this style:
> lemma "XXX = ZZZ"
> proof -
> have "XXX = AAA" sorry
> have "ZZZ = BBB" sorry
> also have "... = AAA" sorry (* breaks here *)
> ultimately show ?thesis by simp
> 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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and