*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*: Wed, 28 Apr 2010 22:56:44 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <n2hcc2478ab1004281329pa87e8b54r3793062ee133f464@mail.gmail.com>*References*: <6031272389962@web71.yandex.ru> <k2mcc2478ab1004280945gb510d767maf21c86aad9e0ab5@mail.gmail.com> <4BD897BF.3010405@in.tum.de> <n2hcc2478ab1004281329pa87e8b54r3793062ee133f464@mail.gmail.com>

I might summarize it this way: Locale interpretation transforms a generic theory into a concrete one. What we're looking for is a way to transform a *concrete* theory into a *different* concrete one (or a new generic one, as the case may be). - Brian

- Steven

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

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

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

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

- 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