| changeset 3224 | cf451e182bf0 |
| parent 3052 | 41ec301eb062 |
| 3223:c9a1c6f50ff5 | 3224:cf451e182bf0 |
|---|---|
1 (*<*) |
1 (*<*) |
2 theory Slides9 |
2 theory Slides9 |
3 imports "~~/src/HOL/Library/LaTeXsugar" "Nominal" |
3 imports "~~/src/HOL/Library/LaTeXsugar" "../Nominal/Nominal2" |
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) |