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 sketis.net> 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