Re: [isabelle] A constant become a free variable
On Wed, 4 Dec 2013, Yannick Duchêne (Hibou57) wrote:
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
The basic substitution rules of Isabelle/HOL directly refer to =, not ==.
This is also relevant to calculational reasoning, e.g. see
print_trans_rules. (That gives only very limited support for some basic
Pure reasoning with ==).
Some other tools go to the bottom of Pure and use == internally, such as
the Simplifier itself (which is somewhat independent of the object-logic).
This is also one of several points in the system where both = and == are
allowed in user input, but this duplication of interfaces is not
That was important in the past, because the primite 'defs' command was
used routinely in user theories, and thus there was considerable mix-up of
connectives. For many years already, the 'definition' command allows to
use = of Isabelle/HOL, just like other specification elements that are
proper to HOL.
This archive was generated by a fusion of
Pipermail (Mailman edition) and