Re: [isabelle] Syntax issue: lost between HOL and Isar

Le Wed, 01 Aug 2012 23:30:18 +0200, Gottfried Barrow <gottfried.barrow at> 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 "isabelle-21c42b095c84\doc-src\IsarRef\Thy".

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)
      case 0
      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 that point.

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 (red‑face)

“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

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