*To*: Lars Hupel <hupel at in.tum.de>, Lars Noschinski <noschinl at in.tum.de>*Subject*: Re: [isabelle] Correct handling of fixed and free variables*From*: Makarius <makarius at sketis.net>*Date*: Thu, 27 Jun 2013 11:52:54 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <51AF1271.3090402@in.tum.de>*References*: <kolktt$53l$1@ger.gmane.org> <51AF1271.3090402@in.tum.de>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Wed, 5 Jun 2013, Lars Noschinski wrote:

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 endThese are two separate issues: if we want to use schematic variablesas"holes" in the breakpoint, we need a method, whichv handles both bound andunbound schematic variables.If on the other hand we want to use free variables for the holes then thereis this issue which variables are too be generalized.

The general scheme looks like this: foobar for x y z

Makarius

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

**Re: [isabelle] Correct handling of fixed and free variables***From:*Lars Noschinski

- Previous by Date: Re: [isabelle] normalization method introduces schematic type variables in HOL/Word types
- Next by Date: [isabelle] partial_function: order of variables in induction rule
- Previous by Thread: Re: [isabelle] Correct handling of fixed and free variables
- Next by Thread: [isabelle] post-doctoral position at MSR-INRIA, Paris
- 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