[isabelle] keyword defines
in the Isar reference manual, "defines" is explained as
defines a: x ≡ t defines a previously declared parameter. This is
similar to def within a proof (cf. §6.2.1), but defines takes an
equational proposition instead of variable-term pair. The left-
hand side of the equation may have additional arguments, e.g.
“defines f x 1 ... x n ≡ t”.
This vaguely resembles section 16.5.2 Extension by constant specification in Gordon & Melham: Introduction to HOL.
Is this reference the source of inspiration for this Isar keyword?
And, is there a written account on the basic definitional mechanisms of Isabelle, explained model theoretically?
This archive was generated by a fusion of
Pipermail (Mailman edition) and