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



Hi,

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

http://www4.informatik.tu-muenchen.de/~nipkow/pubs/tphols08t.pdf

"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:

http://www.cl.cam.ac.uk/research/hvg/isabelle/overview.html

"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?

Thanks

John





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