| changeset 2465 | 07ffa4e41659 |
| parent 2381 | fd85f4921654 |
| child 2471 | 894599a50af3 |
| 2464:f4eba60cbd69 | 2465:07ffa4e41659 |
|---|---|
1 (*<*) |
1 (*<*) |
2 theory Paper |
2 theory Paper |
3 imports "../Nominal/NewParser" "LaTeXsugar" |
3 imports "../Nominal/Nominal2" "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" |