[isabelle] Syntax issue: lost between HOL and Isar
Hi all proof lovers,
After the Isar reference, I typed this in Isabelle/jEdit:
fix n :: nat
have "P n"
proof (induct n)
show ?case sorry
case (Suc n)
from Suc.hyps show ?case sorry
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
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.” 
“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