| changeset 203 | 5d724fe0e096 |
| parent 24 | f72c82bf59e5 |
| child 212 | 3629680a20a2 |
| 202:09e6f3719cbc | 203:5d724fe0e096 |
|---|---|
1 (*<*) |
1 (*<*) |
2 theory Slides |
2 theory Slides |
3 imports "LaTeXsugar" |
3 imports "~~/src/HOL/Library/LaTeXsugar" |
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) |