| changeset 2303 | c785fff02a8f |
| parent 2186 | 762a739c9eb4 |
| child 2203 | 530b0adbcf77 |
| 2302:c6db12ddb60c | 2303:c785fff02a8f |
|---|---|
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" |