[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?

- Gergely

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