Isabelle/Isar supports basically three kinds of "comments":
(1) Source comments (* like this *) which are stripped from the text
as it is being processed, i.e. they behave like comments in most
programming languages, or % in TeX.
(2) Document comments -- {* like this *} which are considered part of
the formal langaguage and are included in the final typesetting.
(3) Explicit markup commands, notably
chapter {* ... *}
section {* ... *}
subsection {* ... *}
text {* ... *}
These are full commands, just like 'theorem' or 'proof', but the do
not affect the logical context.
The argument text {* ... *} of document comments and markup commands can
refer to logical entities from the context of the text, by using document
antiquotations. For example:
text {* blah blah @{term "x + y = z"} blah blah @{thm lemma1} ... *}
These antiquotations are checked according to the full logical context,
and pretty printed with the syntax of the context (although I would prefer
annotating the original input source, instead of printing internal
entities).
Since this thread was initially about meta data for theories, what we have
in Isabelle/Isar is only this:
header {* ... *}
theory A ...
begin
...
end
Here the 'header' provides free-form text, it is usually typeset like
'section'. Adding extra commands for 'author' etc. would be straight
forward, but we have never really needed this yet. In Isabelle/Isar
documents the title/author is usually part of the outermost root.tex that
assembles all the generated LaTeX sources in the end.
Makarius