Re: [isabelle] Function Definitions Within Locales

On Mon, 2010-09-13 at 16:47 +0200, Florian Haftmann wrote:
> Hi Matej,
> This in the strictest sense is not possible.  You can circumvent this in
> one of the following ways.
> a) Introduce intermediate locale where you just define the function
> formally and then import this locale into the main locale with
> assumptions about the function
> b) Turn the function itself into a parameter of the locale and assume
> its desired properties explicitly.

Mhm, I see. I was already eyeing the intermediate locale approach. It is
actually quite a natural 'workaround.'

Thank you very much indeed.


Attachment: signature.asc
Description: This is a digitally signed message part

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