*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] Proof by analogy and proof stability in Isabelle*From*: Steven Obua <steven at obua.de>*Date*: Fri, 30 Apr 2010 17:46:59 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <y2tcc2478ab1004300732qd8279540yf952a066e0d9c50e@mail.gmail.com>*References*: <6031272389962@web71.yandex.ru> <4BD91699.8020401@in.tum.de> <1272538820.2300.49.camel@weber> <4BD978ED.2000106@in.tum.de> <609753366.332953.1272545192863.JavaMail.open-xchange@oxltgw05.schlund.de> <y2tcc2478ab1004300732qd8279540yf952a066e0d9c50e@mail.gmail.com>

"Transferring content" is exactly what an external representation of proof objects would allow you to do. A format like Joe Hurd's OpenTheory is designed primarily for transferring theorems between completely different theorem provers, but the same idea could also be useful for transferring theorems between different versions of the *same* theorem prover.And yes, this meansthat at least a part of the versioning system becomes part of thetrusted kernelof the proof assistant.The great thing about using proof objects is that you don't need to trust any new code.

- Steven

**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:*steven at obua.de

**Re: [isabelle] Proof by analogy and proof stability in Isabelle***From:*Brian Huffman

- Previous by Date: [isabelle] 2 open PhD positions in formal development and testing of secure software
- 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