Re: [isabelle] TERM exception in fologic.ML
On Sat, 23 Jan 2016, Slawomir Kolodynski via Cl-isabelle-users wrote:
Back in October 2014 I reported an error that I encountered when
updating IsarMathLib to Isabelle 2014. The error is still there in
Yes, for the historical record the thread started here:
That was after the Isabelle2014 release. For the release process of
Isabelle2015, it was discussed again here:
The conclusion: no conclusion yet. It not easy to change the situation
without revisiting the "blast" implementation, and it was not done in the
meantime. So it won't happen for Isabelle2016.
This is not a very important problem for me as I can work around it, but
maybe it's good to know that it is still there.
For the record on this mailing list: in October 2014 the workaround was
using [[hypsubst_thin]] by auto
Of course you can also do this more globally via "declare
[[hypsubst_thin]]", although you loose the potential benefit of the
hypsubst change behind this (see NEWS of Isabelle2014).
This archive was generated by a fusion of
Pipermail (Mailman edition) and