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:

notepad
begin

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

end

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".


	Makarius





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