*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] Proof by analogy and proof stability in Isabelle*From*: Peter Lammich <peter.lammich at uni-muenster.de>*Date*: Thu, 29 Apr 2010 12:02:54 +0200*Cc*: isabelle-users at cl.cam.ac.uk, Paul Jackson <pbj at inf.ed.ac.uk>, Bogdan Grechuk <grechukbogdan at yandex.ru>, Jaroslav Sevcik <jarin.sevcik at gmail.com>*In-reply-to*: <4BD95163.5060402@in.tum.de>*References*: <6031272389962@web71.yandex.ru> <4BD91699.8020401@in.tum.de> <21347.1272529832@muckart.inf.ed.ac.uk> <4BD95163.5060402@in.tum.de>*User-agent*: Thunderbird 2.0.0.24 (X11/20100318)

Tobias Nipkow schrieb:

This is the killer, I believe: "Moreover, if the proofs of intermediate lemmas will also be unpacked, this proof would remain correct even if some intermediate lemmas disappear in the new version!" Otherwise replaying proofs is uncritical.

by preserving the modularity of the original proof.

**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:*Tobias Nipkow

- 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