Re: [isabelle] A constant become a free variable
On Wed, 04 Dec 2013 13:22:15 +0100, Makarius <makarius at sketis.net> wrote:
The PIDE markup seen in the input or output represents certain aspects of
the formal processing by the prover. This sometimes exposes more
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
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and