Re: [isabelle] A constant become a free variable

Le Wed, 04 Dec 2013 16:00:56 +0100, Makarius <makarius at> a écrit:

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.

Does that mean substitution/simplification is not expressed with “==” but “=” instead ? I always though “==” was the standard for that purpose with logic.

“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

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