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


I see that Isabelle/Pure being referred to as a meta-logic:


"The Isabelle/Pure meta-logic allows the formalization of the syntax
and inference rules of a broad range of object-logics"

and as a framework logic:


"These are formulated within Isabelle's logical framework
Isabelle/Pure, which is suitable for a variety of formal calculi (e.g.
axiomatic set theory)."

My naive understanding is that a meta-logic encodes object-logics.
Since Isabelle/Pure encodes Isabelle/HOL within it, it's a meta-logic.
If so, how come it's called a framework logic elsewhere?



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