[isabelle] Syntax issue: lost between HOL and Isar



Hi all proof lovers,

After the Isar reference, I typed this in Isabelle/jEdit:

  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

As the syntax from the PDF is not always exact (mainly characters issues), I though there was an error there too, and felt “(Suc n)” should be enclosed in quote, as an HOL expression. But doing so, I get this in the Output pan:

  Unknown case: "(Suc n)"

Is “(Suc n)”, and HOL or Isar expression? If that's an HOL expression as I believe, then why do I get that error report?


--
“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.