# Re: [isabelle] Can I assume an interpretation

On Mon, 7 Apr 2008, David Streader wrote:
> p.s. Isar is proofs have been very much more robust than any proofs I
> previously constructed in Isabelle.
BTW, Isar proofs work out more smoothly when presenting statements in
natural rule format. This prevents having to walk through the outermost
structure first, both in the proof and the application of the result later
on. E.g. compare these two versions:
lemma transitive1: "a <= b --> b <= c --> a <= c"
proof
assume ab: "a <= b"
show "b <= c --> a <= c"
proof
assume bc: "b <= c"
show "a <= c"
using ab bc sorry
qed
qed
lemma transitive2:
assumes ab: "a <= b"
and bc: "b <= c"
shows "a <= c"
proof -
show ?thesis using ab bc sorry
qed
Makarius

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