src/Pure/General/comment.ML
18 months ago wenzelm 2018-01-14 clarified signature;
18 months ago wenzelm 2018-01-14 clarified modules: uniform notion of formal comments;