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

On 10/30/2012 03:51 AM, Gottfried Barrow wrote:
On 10/28/2012 11:58 PM, Christian Sternagel wrote:


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.
I tried to achieve something very similar in my PhD-thesis (the content is not really textbook-like, but the presentation was intended for people that do not know Isabelle/HOL). Just ignoring the content you could have a look whether this way of presentation could be used in your case.

However, it was a huge overhead over the actual formalization to present it this way ;). (And I found it necessary to explain at least a bit about Isabelle in the beginning.)

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



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.