Re: [isabelle] Correct handling of fixed and free variables

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

These are two separate issues: if we want to use schematic variables as"holes" in the breakpoint, we need a method, whichv handles both bound and unbound schematic variables.

If on the other hand we want to use free variables for the holes then there is this issue which variables are too be generalized.

  -- Lars

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