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



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.