| changeset 2747 | a5da7b6aff8f |
| parent 2736 | 61d30863e5d1 |
| 2746:6aa98a113e6c | 2747:a5da7b6aff8f |
|---|---|
1 (*<*) |
1 (*<*) |
2 theory Paper |
2 theory Paper |
3 imports "../Nominal/Nominal2_Base" |
3 imports "../Nominal/Nominal2_Base" |
4 "../Nominal/Atoms" |
4 "../Nominal/Atoms" |
5 "LaTeXsugar" |
5 "~~/src/HOL/Library/LaTeXsugar" |
6 begin |
6 begin |
7 |
7 |
8 notation (latex output) |
8 notation (latex output) |
9 sort_of ("sort _" [1000] 100) and |
9 sort_of ("sort _" [1000] 100) and |
10 Abs_perm ("_") and |
10 Abs_perm ("_") and |