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:

http://isabelle.in.tum.de/repos/isabelle/archive/21c42b095c84.tar.gz

The link that would get you to the link for that file is here:

http://isabelle.in.tum.de/repos/isabelle/

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:

  notepad
  begin
    fix n :: nat
    have "P n"
    proof (induct n)
      case 0
      show ?case sorry
    next
      case (Suc n)
      from Suc.hyps show ?case sorry
    qed
  end

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.