| changeset 2184 | 665b645b4a10 |
| parent 2176 | 5054f170024e |
| child 2186 | 762a739c9eb4 |
| 2182:9d0b94e3662f | 2184:665b645b4a10 |
|---|---|
1 (*<*) |
1 (*<*) |
2 theory Paper |
2 theory Paper |
3 imports "../Nominal/Test" "LaTeXsugar" |
3 imports "../Nominal/Test" "../Nominal/FSet" "LaTeXsugar" |
4 begin |
4 begin |
5 |
5 |
6 consts |
6 consts |
7 fv :: "'a \<Rightarrow> 'b" |
7 fv :: "'a \<Rightarrow> 'b" |
8 abs_set :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" |
8 abs_set :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" |