Re: [isabelle] emergence of "TERM _" (using quickcheck and nitpick)

On Wed, 26 Nov 2014, Stefan Berghofer wrote:

The failure of your tactic is caused by the following changeset:

In order to do "more static checking of proof methods", a proof method is first applied to the dummy theorem "TERM _" before it gets applied to the actual proof state.

That changeset is indeed quite important to produce early failure of
tactics that are not done right -- the intention was a different one, but this is a good additional benefit.

Note that the explanation why the TERM occurs is merely informative -- these things belong to the system internals: they change quite a bit over the years.


          945,396 people so far

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