*To*: Buday Gergely <gbuday at karolyrobert.hu>*Subject*: Re: [isabelle] keyword defines*From*: Makarius <makarius at sketis.net>*Date*: Tue, 23 Feb 2016 14:35:14 +0100 (CET)*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <C32D3449D568C445AB18C60817FABFE101AC727CE7FD@ingrid.foiskola.krf>*References*: <C32D3449D568C445AB18C60817FABFE101AC727CE7FD@ingrid.foiskola.krf>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Tue, 23 Feb 2016, Buday Gergely wrote:

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”.

The 'defines' context element is just a form to write fixes x assumes "x == t"

This vaguely resembles section 16.5.2 Extension by constantspecification in Gordon & Melham: Introduction to HOL.

And, is there a written account on the basic definitional mechanisms ofIsabelle, explained model theoretically?

Makarius

**References**:**[isabelle] keyword defines***From:*Buday Gergely

- Previous by Date: [isabelle] announcing AFP 2016
- Next by Date: Re: [isabelle] Isabelle references and support
- Previous by Thread: [isabelle] keyword defines
- Next by Thread: [isabelle] Isabelle references and support
- Cl-isabelle-users February 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list