*To*: "steven at obua.de" <steven at obua.de>*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:32:13 -0700*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <609753366.332953.1272545192863.JavaMail.open-xchange@oxltgw05.schlund.de>*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>*Sender*: huffman.brian.c at gmail.com

On Thu, Apr 29, 2010 at 5:46 AM, steven at obua.de <steven at obua.de> wrote: > > b) Develop a versioning system that not only manages source code (like it is > currently done) but also content (theories, theorems, proofs, and so on). Part > of this versioning system is also a mechanism on how to transfer content from > one version to another "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 means > that at least a part of the versioning system becomes part of the trusted kernel > of the proof assistant. The great thing about using proof objects is that you don't need to trust any new code. - Brian

**Follow-Ups**:**Re: [isabelle] Proof by analogy and proof stability in Isabelle***From:*Steven Obua

**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

- 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