For the authorship of files and the biblio please use source comments
(* _ *) instead of the markup command
text < _ >, at the top and bottom of the files, respectively. Indeed, we will eventually submit to the AFP or/and to a journal, so we will have a .bib file anyway. Moreover, for the biblio please use BibTeX entries.
Of course comments
text < _ > within the body of a theory are fine, but don't lose too much time on them right now, we can still work on them later during the documentation preparation. However, if you have collaborators, or even for yourself, use enough source comments.
I updated the theory files accordingly in my master branch.
@Hanna Lachnitt @Yijun He
Last updated: Jul 15 2022 at 23:21 UTC