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:

 http://isabelle.in.tum.de/repos/isabelle/rev/31e283f606e2

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.


	Makarius

----------------------------------------------------------------------------
                  http://stop-ttip.org  945,396 people so far
----------------------------------------------------------------------------




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