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



On 02.08.2012 15:58, Gottfried Barrow wrote:
So some HOL syntax is defined with Isar commands, and some HOL syntax is
defined with ML, where some HOL syntax is added as outer syntax.

"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).

Both syntaxes can be extended, but after bootstrapping, the outer syntax usually stays pretty static; where as the inner syntax is changed with any definition or syntax annotation you issue. I think, by default there is no tool on the Isar level which would modify the outer syntax (just as there is no construct on the term level, which would modify the inner syntax).

  -- Lars.





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