Re: [isabelle] Is Isabelle/Pure really a meta-logic?

Regarding the remark about higher-order abstract syntax, should one call
the Term datatype in Term.ML HOAS? If I understand correctly, Its purpose
is to bind the meta-language to the the object-language.



On Wed, Aug 22, 2012 at 7:51 PM, Lawrence Paulson <lp15 at> wrote:

> Also called a meta-logical-framework. I prefer that name as being more
> uniform.
> Larry
> On 22 Aug 2012, at 19:07, Randy Pollack <rpollack0 at> wrote:
> > A metalogic formalizes the construction of the syntax of the object
> > logic, usually as true inductive objects, allowing induction over the
> > construction of these objects.

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