*To*: Jeremy Dawson <Jeremy.Dawson at anu.edu.au>*Subject*: Re: [isabelle] Lifting variables in theorem*From*: Makarius <makarius at sketis.net>*Date*: Mon, 3 Feb 2014 11:11:48 +0100 (CET)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <52EE6127.7080707@anu.edu.au>*References*: <4B8F827F-81E0-4526-A3C3-07D35B11E013@chalmers.se> <52EC64E4.30405@anu.edu.au> <alpine.LNX.2.00.1402011236190.15165@lxbroy10.informatik.tu-muenchen.de> <52ED0D37.1070908@anu.edu.au> <alpine.LNX.2.00.1402011914460.25155@lxbroy10.informatik.tu-muenchen.de> <52EE6127.7080707@anu.edu.au>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Mon, 3 Feb 2014, Jeremy Dawson wrote:

My whole point is that it should NOT be difficult for anyone to runproofs today which were written in 2005 (or, indeed, much earlier).

That problem is de-facto solved since 2004: Isabelle/AFP http://afp.sf.net

The Proof.context was introduced shortly after Isabelle98 in order to support structured proofs in Isar. Later it turned out as generally useful concept, so after 2000 or so, more and more tools became context-aware. That made a big difference: before there was unsure tinkering with free and schematic variables by hand, never being sure if they could clash with other variables from the environment; afterwards things actually started working reliably.I'm not clear what the problem is that you are describing but it doesn'tsound like anything I have issues with in my work.

Makarius

**Follow-Ups**:**Re: [isabelle] Lifting variables in theorem***From:*Jeremy Dawson

**References**:**Re: [isabelle] Lifting variables in theorem***From:*Jeremy Dawson

**Re: [isabelle] Lifting variables in theorem***From:*Makarius

**Re: [isabelle] Lifting variables in theorem***From:*Jeremy Dawson

**Re: [isabelle] Lifting variables in theorem***From:*Makarius

**Re: [isabelle] Lifting variables in theorem***From:*Jeremy Dawson

- Previous by Date: [isabelle] Large bodies of knowledge
- Next by Date: Re: [isabelle] [Coq-Club] Large bodies of knowledge
- Previous by Thread: Re: [isabelle] Lifting variables in theorem
- Next by Thread: Re: [isabelle] Lifting variables in theorem
- Cl-isabelle-users February 2014 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