equal
deleted
inserted
replaced
3 |
3 |
4 %body% |
4 %body% |
5 |
5 |
6 <!-- _GP_ distname --> documentation is included here as browsable PDF |
6 <!-- _GP_ distname --> documentation is included here as browsable PDF |
7 for convenience. These documents are also part of the standard |
7 for convenience. These documents are also part of the standard |
8 Isabelle <a href="dist/">distribution</a>. |
8 Isabelle <a href="dist/index.html">distribution</a>. |
9 |
9 |
10 <!-- _GP_ include("$pwd/docu-contents.main") --> |
10 <!-- _GP_ include("$pwd/docu-contents.main") --> |