changeset 2747 | a5da7b6aff8f |
parent 2746 | 6aa98a113e6c |
child 2754 | 2a3a37f29f4f |
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 "../Nominal/Nominal2_Abs" |
5 "../Nominal/Nominal2_Abs" |
6 "LaTeXsugar" |
6 "~~/src/HOL/Library/LaTeXsugar" |
7 begin |
7 begin |
8 |
8 |
9 abbreviation |
9 abbreviation |
10 UNIV_atom ("\<allatoms>") |
10 UNIV_atom ("\<allatoms>") |
11 where |
11 where |