Proof annotation issues in Isabelle

Sara Kalvala

Annotations are enhanced comments that can be added to terms to store information of different types, and can provide a useful method for enhancing the proof environment. I have previously described a methodology for implementing annotations in the HOL system. In this talk I will discuss the issues that arise in their implementation in Isabelle, and show how they can be used to deal with several issues that are of interest to many Isabelle users, such as visualizing the structure of proofs and the use of proof terms.