| changeset 2186 | 762a739c9eb4 |
| parent 2184 | 665b645b4a10 |
| child 2203 | 530b0adbcf77 |
| 2185:1cf20169660c | 2186:762a739c9eb4 |
|---|---|
1 (*<*) |
1 (*<*) |
2 theory Paper |
2 theory Paper |
3 imports "../Nominal/Test" "../Nominal/FSet" "LaTeXsugar" |
3 imports "../Nominal/Test" "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" |