Re: [isabelle] Proof by analogy and proof stability in Isabelle



Lawrence Paulson wrote:
Another small point: if you use sledgehammer to generate metis calls,
these will be stable, because they explicitly list all the theorems
involved.

But even metis calls can break when the library changes under your feet. :-/

Alex





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