Thanks for this interesting and enlightening discussion.
I have always had an intuitive appreciation of the meta-logic in
Isabelle. I find it clarifies the both the modeling and proof
activities profoundly.
I would be interested also in a discussion of an important place where
the meta-logi
In the beginning, it was precisely as you describe. Even now, Isabelle/ZF and
Isabelle/CTT continue to distinguish metalevel functions (which in ZF would be
seen as operators or class functions) from the functions of the formalism. I
published and implemented an early formalisation of simple typ
