| changeset 2568 | 8193bbaa07fe |
| parent 2467 | 67b3933c3190 |
| child 2736 | 61d30863e5d1 |
| 2567:41137dc935ff | 2568:8193bbaa07fe |
|---|---|
1 (*<*) |
1 (*<*) |
2 theory Paper |
2 theory Paper |
3 imports "../Nominal-General/Nominal2_Base" |
3 imports "../Nominal/Nominal2_Base" |
4 "../Nominal-General/Nominal2_Eqvt" |
4 "../Nominal/Nominal2_Eqvt" |
5 "../Nominal-General/Atoms" |
5 "../Nominal/Atoms" |
6 "LaTeXsugar" |
6 "LaTeXsugar" |
7 begin |
7 begin |
8 |
8 |
9 notation (latex output) |
9 notation (latex output) |
10 sort_of ("sort _" [1000] 100) and |
10 sort_of ("sort _" [1000] 100) and |