src/Pure/Thy/document_antiquotations.ML
changeset 82892 45107da819fc
parent 81628 e5be995d21f0