Re: [isabelle] Syntax issue: lost between HOL and Isar
Le Tue, 07 Aug 2012 03:30:52 +0200, Gottfried Barrow
<gottfried.barrow at gmx.com> 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
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.” 
“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