equal
deleted
inserted
replaced
6 |
6 |
7 text {* |
7 text {* |
8 |
8 |
9 \begin{itemize} |
9 \begin{itemize} |
10 \item You can make references to other Isabelle manuals using the |
10 \item You can make references to other Isabelle manuals using the |
11 reference names from those manuals. For this the following |
11 reference names from those manuals. To do this the following |
12 four latex commands are defined: |
12 four latex commands are defined: |
13 |
13 |
14 \begin{center} |
14 \begin{center} |
15 \begin{tabular}{l|c|c} |
15 \begin{tabular}{l|c|c} |
16 & Chapters & Sections\\\hline |
16 & Chapters & Sections\\\hline |