*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Free variable dead horse beat; getting two equiv formulas after either one is axiomatized*From*: Christian Sternagel <c-sterna at jaist.ac.jp>*Date*: Tue, 30 Oct 2012 10:21:17 +0900*In-reply-to*: <508ED014.3000009@gmx.com>*References*: <508B968B.4070709@gmx.com> <508BEFEC.907@jaist.ac.jp> <508CF0DC.8030301@gmx.com> <508E0D04.1050003@jaist.ac.jp> <508ED014.3000009@gmx.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:16.0) Gecko/20121016 Thunderbird/16.0.1

On 10/30/2012 03:51 AM, Gottfried Barrow wrote:

On 10/28/2012 11:58 PM, Christian Sternagel wrote: Christian,The most important question: What is your actual application anyway?This was your second to the last question. You say it's the most important, so I move it up here, since I get wordy below. The application is implementing certain mathematical textbooks in Isabelle, until I get to a level to where I use Isabelle to implement original research. The style is educational, textbook writing. Discussion, example, theorem, proof, exercise, repeat. The original research part will be the hardest part to achieve, especially because it will be so time consuming to build up to that level. I at least try to end up having made an educational contribution.

http://www.jaist.ac.jp/~c-sterna/publications/PhD-thesis.pdf

If you (or anyone else) are interested I can send you the sources later. cheers chris

**Follow-Ups**:

**References**:**[isabelle] Free variable dead horse beat; getting two equiv formulas after either one is axiomatized***From:*Gottfried Barrow

**Re: [isabelle] Free variable dead horse beat; getting two equiv formulas after either one is axiomatized***From:*Christian Sternagel

**Re: [isabelle] Free variable dead horse beat; getting two equiv formulas after either one is axiomatized***From:*Gottfried Barrow

**Re: [isabelle] Free variable dead horse beat; getting two equiv formulas after either one is axiomatized***From:*Christian Sternagel

*From:*Gottfried Barrow

- Previous by Date: Re: [isabelle] Free variable dead horse beat; getting two equiv formulas after either one is axiomatized
- Next by Date: Re: [isabelle] Free variable dead horse beat; getting two equiv formulas after either one is axiomatized
- Previous by Thread: Re: [isabelle] Free variable dead horse beat; getting two equiv formulas after either one is axiomatized
- Next by Thread: Re: [isabelle] Free variable dead horse beat; getting two equiv formulas after either one is axiomatized
- Cl-isabelle-users October 2012 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