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 Isabelle2016-RC1.

Yes, for the historical record the thread started here:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2014-October/msg00116.html

That was after the Isabelle2014 release. For the release process of Isabelle2015, it was discussed again here: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-April/msg00303.html

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 like this:

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


	Makarius





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