| changeset 2330 | 8728f7990f6d |
| parent 2218 | 502eaa199726 |
| child 2331 | f170ee51eed2 |
| 2329:df3a952c6a67 | 2330:8728f7990f6d |
|---|---|
1 (*<*) |
1 (*<*) |
2 theory Paper |
2 theory Paper |
3 imports "../Nominal/Test" "LaTeXsugar" |
3 imports "../Nominal/NewParser" "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" |