equal
deleted
inserted
replaced
1 (* Title: antiquote_setup.ML |
1 (* Title: Doc/antiquote_setup.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Makarius |
3 Author: Makarius |
4 |
4 |
5 Auxiliary antiquotations for Isabelle manuals. |
5 Auxiliary antiquotations for Isabelle manuals. |
6 *) |
6 *) |