| changeset 3224 | cf451e182bf0 |
| parent 2748 | 6f38e357b337 |
| 3223:c9a1c6f50ff5 | 3224:cf451e182bf0 |
|---|---|
1 (*<*) |
1 (*<*) |
2 theory Slides3 |
2 theory Slides3 |
3 imports "~~/src/HOL/Library/LaTeXsugar" "Nominal" |
3 imports "~~/src/HOL/Library/LaTeXsugar" "../Nominal/Nominal2" |
4 begin |
4 begin |
5 |
5 |
6 declare [[show_question_marks = false]] |
6 declare [[show_question_marks = false]] |
7 |
7 |
8 notation (latex output) |
8 notation (latex output) |