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
This archive was generated by a fusion of
Pipermail (Mailman edition) and