equal
deleted
inserted
replaced
1 |
1 |
2 theory Antiquotes |
2 theory Antiquotes |
3 imports "../Base" |
3 imports "../Base" |
4 begin |
4 begin |
5 |
5 |
6 section {* Useful Document Antiquotations *} |
6 section {* Useful Document Antiquotations\label{rec:docantiquotations} *} |
7 |
7 |
8 text {* |
8 text {* |
9 {\bf Problem:} |
9 {\bf Problem:} |
10 How to keep your ML-code inside a document synchronised with the actual code?\smallskip |
10 How to keep your ML-code inside a document synchronised with the actual code?\smallskip |
11 |
11 |