src/Pure/General/comment.ML
changeset 82249 bdefffffd05f
parent 70229 c03f381fd373