[isabelle] Friendly THY [was, Free variable dead horse beat; getting two equiv formulas after either one is axiomatized]

On 10/27/2012 9:30 AM, Christian Sternagel wrote:
first of all, the way you are using symbols in comments is rather non-conventional and makes the THY file a bit cluttered with unnecessary noise. Since typical Isabelle users might prefer to consult the THY file over the generated PDF file that is unfortunate.


I reply to the easy part first, though important. The other part of your reply is the important technical part, and I'm still thinking about that part.

First, I'll make two general statements: (1) There's no good solution. (2) With Isabelle, I'm out to cater to the market, however I need to do that.

I have, at times, put a lot of thought into how I should ask code related questions here. My short answer is usually, "Use ASCII".

Part of the problem is there are two main markets for proof assistants: the world of mathematics and the world of computer science.

Those in the world of computer science are, by default, programmers. Those in the world of mathematics, by and large, aren't programmers at all, or only have basic programming skills; consequently, they can sometimes be hostile to unsugarcoated things of a programming nature.

Trying to keep this short, I think part of my solution to catering to the two markets is to create at least two different THYs, along with the PDFs. But then, I can't attach 4 files to every email sent to this list. So maybe I'll put them up somewhere on the web and provide links in the email. I'd have to refine my scripts to create an ASCII version which isn't completely non-verbose.

In the future, if have more suggestions about how I should give you my code, please make those suggestions.


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