[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