Re: [isabelle] Lifting variables in theorem
On 02/03/2014 09:11 PM, Makarius wrote:
On Mon, 3 Feb 2014, Jeremy Dawson wrote:
My whole point is that it should NOT be difficult for anyone to run
proofs today which were written in 2005 (or, indeed, much earlier).
That problem is de-facto solved since 2004: Isabelle/AFP
You merely need to put your material into shape (according to minimal
standards that are routine today) and submit it to the editors of the
archive. Afterwards it is usually maintained "automagically" to work
with current Isabelle versions, but in extreme cases the editors might
ask for you for assistance.
I've been told similar things on occasions before, and it turns out not
to be true. Unless (in this case), your "minimal standards" means
rewriting everything in Isar. Which, as my previous email pointed out,
is not on, since I'm guessing my latest effort involves three to four
hundred thousand tactic applications.
If I'm wrong about this, please clarify
This archive was generated by a fusion of
Pipermail (Mailman edition) and