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"
assume ab: "a <= b"
show "b <= c --> a <= c"
assume bc: "b <= c"
show "a <= c"
using ab bc sorry
assumes ab: "a <= b"
and bc: "b <= c"
shows "a <= c"
show ?thesis using ab bc sorry
This archive was generated by a fusion of
Pipermail (Mailman edition) and