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 cam.ac.uk> wrote:
> Also called a meta-logical-framework. I prefer that name as being more
> 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