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