*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Correct handling of fixed and free variables*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Wed, 05 Jun 2013 12:26:57 +0200*In-reply-to*: <kolktt$53l$1@ger.gmane.org>*References*: <kolktt$53l$1@ger.gmane.org>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:10.0.12) Gecko/20130116 Icedove/10.0.12

On 04.06.2013 23:07, Lars Hupel wrote:

To summarize the constraints: I'd like to have a `Proof.context`-aware term parsing, which works correctly for existing schematic and locally fixed variables. Lars Noschinski also pointed out that care needs to be taken of these two different kinds of fixed variables: notepad begin { have P sorry } note A = this { fix P have P sorry } note B = this end

-- Lars

**Follow-Ups**:**Re: [isabelle] Correct handling of fixed and free variables***From:*Makarius

**References**:**[isabelle] Correct handling of fixed and free variables***From:*Lars Hupel

- Previous by Date: [isabelle] Correct handling of fixed and free variables
- Next by Date: [isabelle] post-doctoral position at MSR-INRIA, Paris
- Previous by Thread: [isabelle] Correct handling of fixed and free variables
- Next by Thread: Re: [isabelle] Correct handling of fixed and free variables
- Cl-isabelle-users June 2013 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