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



Thank you very much for your suggestions and references, Makarius and
Stefan. I'm updating my code and things work.

Daniel

On 26 November 2014 at 18:24, Makarius <makarius at sketis.net> wrote:

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