# 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.*