| changeset 2748 | 6f38e357b337 |
| parent 2356 | 840a857354f2 |
| child 3224 | cf451e182bf0 |
| 2747:a5da7b6aff8f | 2748:6f38e357b337 |
|---|---|
1 (*<*) |
1 (*<*) |
2 theory Slides2 |
2 theory Slides2 |
3 imports "LaTeXsugar" "Nominal" |
3 imports "~~/src/HOL/Library/LaTeXsugar" "Nominal" |
4 begin |
4 begin |
5 |
5 |
6 notation (latex output) |
6 notation (latex output) |
7 set ("_") and |
7 set ("_") and |
8 Cons ("_::/_" [66,65] 65) |
8 Cons ("_::/_" [66,65] 65) |