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.

Cheers

Steve

On Wed, Aug 22, 2012 at 7:51 PM, Lawrence Paulson <lp15 at cam.ac.uk> 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 gmail.com> 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.