Re: [isabelle] A constant become a free variable
Le Wed, 04 Dec 2013 16:00:56 +0100, Makarius
<makarius at sketis.net> 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
“Syntactic sugar causes cancer of the semi-colons.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and