| changeset 2748 | 6f38e357b337 |
| parent 2358 | 8f142ae324e2 |
| child 3224 | cf451e182bf0 |
| 2747:a5da7b6aff8f | 2748:6f38e357b337 |
|---|---|
1 (*<*) |
1 (*<*) |
2 theory Slides3 |
2 theory Slides3 |
3 imports "LaTeXsugar" "Nominal" |
3 imports "~~/src/HOL/Library/LaTeXsugar" "Nominal" |
4 begin |
4 begin |
5 |
|
6 declare [[show_question_marks = false]] |
|
5 |
7 |
6 notation (latex output) |
8 notation (latex output) |
7 set ("_") and |
9 set ("_") and |
8 Cons ("_::/_" [66,65] 65) |
10 Cons ("_::/_" [66,65] 65) |
9 |
11 |