src/Pure/General/comment.ML
changeset 68204 a554da2811f2
parent 67572 a93cf1d6ba87
child 69891 def3ec9cdb7e