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

On 8/2/2012 10:42 AM, Lars Noschinski wrote:

`"HOL syntax" is not a very useful term here. In Isabelle/Isar, we
``distinguish between outer and inner syntax. The inner syntax is the
``syntax used to input terms (and types). Apart from trivial cases,
``inner syntax needs to be quoted.
`

`The outer syntax is everything else. Most of it is already part of
``Pure (i.e. independent of any logic), mainly everything which makes up
``proof and document structure; but logics often add additional commands
``for logic-specific operations (e.g. "fun" and "inductive" for HOL).
`

I think I have it.

`HOL imports pure, therefore it inherits the Isar language and a default
``set of Isar outer syntax commands, where new outer syntax can be defined
``with "Outer_syntax.command". Everything in a .thy file is Isar syntax
``and everything is HOL syntax, so there's no need to talk about HOL
``syntax, since, again, everything is HOL syntax. We could, however,
``compare Isabelle/HOL syntax with Isabelle/FOL syntax, where they would
``both share the default Isar outer syntax commands.
`

`The word "term" doesn't have a lot of significance to me. I assume you
``mean "lambda calculus term", but I see very little lambda calculus in
``expressions between double quotes, so it doesn't completely help me to
``know what to put in double quotes.
`

`However, it is useful to know that if I see something in double quotes,
``I know it must be either a type or a lambda calculus term, even if the
``lambda calculus doesn't look like lambda calculus.
`
Regards,
GB

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*