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