let me again ask a question about Isabelle proofs in common. Being a formal language professional I wonder why these artefacts in your proof libraries need the abstract language level at all. In my opinion most of the proofs could be specified in context free syntax with the semantics attached to it or having semantics in mind or specified elsewhere. If we had the proofs in a CH(2) pattern we could build transformers to transfer them to and from other formalisms, which in turn would foster exchange with other groups building proof libraries worldwide. Am I wrong or is there a reason for maintaining such a hurdle?