*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] File.use function*From*: Clément Hurlin <Clement.Hurlin at esial.uhp-nancy.fr>*Date*: Mon, 1 May 2006 17:28:54 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <Pine.LNX.4.63.0605011256510.27612@atbroy101.informatic.tu-muenchen.de>*References*: <20060430205454.iszh48cc0s0gwss4@venus.esial.uhp-nancy.fr> <Pine.LNX.4.63.0605011256510.27612@atbroy101.informatic.tu-muenchen.de>*User-agent*: Internet Messaging Program (IMP) H3 (4.1.1)

because they are statically fixed bindings to immutable values.

Understood.

Maybe you were actually thinking about assignable references.

val proof_congr = ref [] val proof_inst = ref [] val _ = use proof_hints_fn proof_hints_fn containing : ( proof_inst := X; proof_congr := Y )

Clément

**Follow-Ups**:**Re: [isabelle] File.use function***From:*Makarius

**References**:**Re: [isabelle] File.use function***From:*Makarius

- Previous by Date: Re: [isabelle] File.use function
- Next by Date: Re: [isabelle] File.use function
- Previous by Thread: Re: [isabelle] File.use function
- Next by Thread: Re: [isabelle] File.use function
- Cl-isabelle-users May 2006 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