Re: [isabelle] A constant become a free variable

On Wed, 04 Dec 2013 13:22:15 +0100, Makarius <makarius at> wrote:

The PIDE markup seen in the input or output represents certain aspects of
the formal processing by the prover. This sometimes exposes more internal
details than make sense to the user.  It needs some further refinements,
but that is part of the concept: more and more useful markup information
is provided and rendered -- this is a continuous process over the years.

OK, so may be it says it's a free variable when it does not already know it's fixed.

The use of Pure equality and HOL.eq_reflection looks a bit strange: you
should bever need that in HOL applications, unless some old forms are
somehow ported.

I've just checked, and “HOL.thy” indeed says “(*admissible axiom*)”. Will try to learn to do without it.

Thanks for the pointers you gave on both topics.

Yannick Duchêne

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