Re: [isabelle] A constant become a free variable
On Wed, 4 Dec 2013, Yannick wrote:
I've just checked, and “HOL.thy” indeed says “(*admissible axiom*)”.
Will try to learn to do without it.
In some sense this belongs to the "implementation" of Isabelle/HOL on top
of the Isabelle/Pure framework.
These days you should hardly ever need == in Isabelle/HOL applications.
This is different to !! and ==>, which have a specific purpose to outline
Natural Deduction rule schemes in a declarative manner, independently of
This archive was generated by a fusion of
Pipermail (Mailman edition) and