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