Re: [isabelle] Problems with Logic.mk_implies + compose_tac

Here is one more trick using more modern concepts -- I have just seen in an incoming changset by Florian Haftmann:


  have "!!x y. x = y ==> y = x"
    apply (fact sym)


In ML this is ProofContext.fact_tac. It unifies rules against each other, without taking the implication structure apart.

The nice thing about using "canonical" soluations is that you can switch between Isar source language and ML back and forth in the exploration. In contrast, odd things like Goal.prove_internal are not part of the Isar infrastructure. This is what I meant by "standing naked in the rain".


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