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



Hi Daniel,

On 11/26/2014 05:47 PM, Makarius wrote:
This ML snipped looks non-canonical in various ways, so it is no surprise that it does not work at all.

this is maybe a bit too hash a criticism. A while ago, I had the very same problem in one of my
tactics that had worked without problems with earlier versions of Isabelle, and it took me several
hours of debugging to find the reason for this behaviour.

concl_of a goal state is its main conclusion, but that is private property of the system as pointed out in the manual.

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. The infrastructure
for proof methods expects "proper" tactics to return Seq.empty when applied to such dummy
theorems, rather than failing with an exception.

Greetings,
Stefan




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