src/Pure/General/comment.ML
changeset 68091 0c7820590236
parent 67572 a93cf1d6ba87
child 69891 def3ec9cdb7e