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

Also called a meta-logical-framework. I prefer that name as being more uniform.

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.