| changeset 2862 | 47063163f333 |
| parent 2856 | e36beb11723c |
| child 2931 | aaef9dec5e1d |
| 2860:25a7f421a3ba | 2862:47063163f333 |
|---|---|
3 imports "~~/src/HOL/Library/LaTeXsugar" |
3 imports "~~/src/HOL/Library/LaTeXsugar" |
4 begin |
4 begin |
5 |
5 |
6 declare [[show_question_marks = false]] |
6 declare [[show_question_marks = false]] |
7 |
7 |
8 (*>*) |
8 section {* Introduction *} |
9 |
9 |
10 |
10 |
11 section {* Introduction *} |
|
12 |
11 |
13 |
12 |
14 (*<*) |
13 (*<*) |
15 end |
14 end |
16 (*>*) |
15 (*>*) |