Re: [isabelle] TERM exception in fologic.ML

Blast was never intended to do anything intelligent in the presence of meta-level connectives, which are much more common now, so some adjustments may be necessary.

> On 28 Apr 2015, at 15:01, Makarius <makarius at> wrote:
> My impression is that blast.ML is a bit non-canonical in many respects, not just superficially due to the use of camel case in the source.  Its use of strip_Trueprop looses information about presence or absence of Trueprop.  Later use of Data.hyp_subst_tac may stumble on that.

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