Re: [isabelle] Syntax issue: lost between HOL and Isar
Le Wed, 01 Aug 2012 23:30:18 +0200, Gottfried Barrow
<gottfried.barrow at gmx.com> a écrit:
You can get the sources for any of the Isabelle2012 documentation.
The direct link is this:
The link that would get you to the link for that file is here:
Thanks Gottfried, those links are worth to be bookmarked :-P
You click on "files" beside "2 months ago Isabelle2012". You would then
click on "gz" at the top of the page.
You unzip the tar file, and for isar-ref.pdf, you find the folder
You then have to search around on those files with grep or something to
find the file that contains the desired code.
I got it, that's in “Synopsis.thy”, and modulo the indentation, that's the
same, there is no quote too:
fix n :: nat
have "P n"
proof (induct n)
show ?case sorry
case (Suc n)
from Suc.hyps show ?case sorry
So, what's the expression type of “(Suc n)” at the line whose text is
“case (Suc n)”? Isn't “(Suc n)” an HOL expression? It appears in the text
as if it was an Isar expression, but I feel sure it's not. I'm lost with
The source files keep you from having to type in the code, keep you from
copying bogus characters from the PDF, and they teach you something
about how the author produced what you see in the PDF.
They also will teach me a bit of LaTex, which I've never practiced
“Syntactic sugar causes cancer of the semi-colons.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and