*To*: Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] Proof by analogy and proof stability in Isabelle*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Fri, 30 Apr 2010 07:45:55 -0700*Cc*: isabelle-users at cl.cam.ac.uk, Tjark Weber <tjark.weber at gmx.de>*In-reply-to*: <E5D672ED-0FFC-4290-BD8D-E3320379C58E@cam.ac.uk>*References*: <6031272389962@web71.yandex.ru> <4BD91699.8020401@in.tum.de> <1272538820.2300.49.camel@weber> <4BD978ED.2000106@in.tum.de> <1272589168.2326.211.camel@weber> <E5D672ED-0FFC-4290-BD8D-E3320379C58E@cam.ac.uk>*Sender*: huffman.brian.c at gmail.com

On Fri, Apr 30, 2010 at 6:21 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote: > I would be surprised if proof stability was the leading issue with users. I certainly do not recall losing much time in the course of a proof development to patching up failing proofs, even though (unlike most ordinary users surely) I invariably use potentially unstable development snapshots. I would suggest that using incremental development snapshots actually makes patching up your proofs *easier*. On occasion I have had significant amounts of trouble getting old proof scripts to work again. The process is most difficult with theories that were developed for older versions of Isabelle: Porting a proof directly from Isabelle 2005 to 2009 can be much more difficult than continuously adapting the same proof to a series of development snapshots. I would suspect that most users have to deal with these large version-jumps more often than the developers do. - Brian

**Follow-Ups**:

**References**:**[isabelle] Proof by analogy and proof stability in Isabelle***From:*grechukbogdan

**Re: [isabelle] Proof by analogy and proof stability in Isabelle***From:*Tobias Nipkow

**Re: [isabelle] Proof by analogy and proof stability in Isabelle***From:*Tjark Weber

**Re: [isabelle] Proof by analogy and proof stability in Isabelle***From:*Tobias Nipkow

**Re: [isabelle] Proof by analogy and proof stability in Isabelle***From:*Tjark Weber

**Re: [isabelle] Proof by analogy and proof stability in Isabelle***From:*Lawrence Paulson

- Previous by Date: Re: [isabelle] Proof by analogy and proof stability in Isabelle
- Next by Date: Re: [isabelle] Proof by analogy and proof stability in Isabelle
- Previous by Thread: Re: [isabelle] Proof by analogy and proof stability in Isabelle
- Next by Thread: Re: [isabelle] Proof by analogy and proof stability in Isabelle
- Cl-isabelle-users April 2010 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