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

Le Tue, 07 Aug 2012 03:30:52 +0200, Gottfried Barrow <gottfried.barrow at> a écrit:
Now I sit on the two ideas and wait to see if I read something that supports one of the two ideas, that HOL inherits Isar and makes it its own, or Isar is a framework that gets stripped away by the backend. Today, right now, I'm leaning towards the idea that much of the Isar gets stripped away.

I believe HOL inherits/use Isar, but I can't prove it (cheese).

Along with this, for others interested in the original question too, here is an evidence that what you write in quotes, is not specifically HOL: you write lemma's conclusion to prove in quotes, and that's obviously not HOL, which I believe is object logic only. Ex. the “==>” is meta‑level logic.

So here comes an updated definitions perhaps, of what you have to put in quotes: you write in quotes, every expressions which involves mix‑fix notations (I don't know any of these outside of quotes), to which is to be added previously mentioned type expressions when not syntactically atomic and names when not simples (ex. containing dash, math symbols and the like).

P.S. I've not read all replies to that thread in deep details so far, so I apologies for any contradictions with what others may have said if ever there are some.

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