changeset 62058 | 1cfd5d604937 |
parent 61814 | 1ca1142e1711 |
child 62153 | df566b87e269 |
--- a/src/Pure/Thy/document_antiquotations.ML Tue Jan 05 13:41:29 2016 +0100 +++ b/src/Pure/Thy/document_antiquotations.ML Tue Jan 05 13:48:51 2016 +0100 @@ -1,4 +1,4 @@ -(* Title: Pure/ML/document_antiquotations.ML +(* Title: Pure/Thy/document_antiquotations.ML Author: Makarius Miscellaneous document antiquotations.