# Re: [isabelle] Definition in (and of) Isabelle/HOL

On Fri, 11 Apr 2014, Rob Arthan wrote:

`Do you do anything to avoid the potential problem whereby two calls of
``new_specification with the same predicate will result in provably equal
``constants if you implement new_specification naively with Hilbert
``choice. E.g., ?x.1 < x < 10 used to define c and d? This is addressed
``in HOL Light along the following lines: it defines a function on the
``natural numbers such that 1 < x(n) < 10 for all n, and then defines c =
``x(42) and d = x(43), assuming that c is the 42nd constant that HOL Light
``has been asked to define.
`

`There is nothing like this in the 'specification' command of Isabelle/HOL,
``but that add-on feature from 2004 got hardly ever used in practice. It
``also fell behind a lot concerning general system infrastructure for
``Isabelle specifications.
`

`I have recently asked around the canonical question if 'specification'
``should be be removed or renovated, and it came out a slight tendency
``towards renovation (after removal of some of its obsolete sub-features).
`

`Locales are indeed better in most situations to work in a context of
``abstract term parameters with some logical premises in the local context.
``Almost all specification mechanisms in Isabelle/HOL are now "localized",
``i.e. work in such hypothetical situations of "fixes" and "assumes", so
``that is a real practical benefit. The cost for it is increasingly complex
``system infrastructure (outside the core logical framework).
`
Makarius

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