equal
deleted
inserted
replaced
1 (* Title: Pure/ML/document_antiquotations.ML |
1 (* Title: Pure/Thy/document_antiquotations.ML |
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 Miscellaneous document antiquotations. |
4 Miscellaneous document antiquotations. |
5 *) |
5 *) |
6 |
6 |