src/Pure/General/comment.ML
changeset 74301 ffe269e74bdd
parent 70229 c03f381fd373