| changeset 2747 | a5da7b6aff8f |
| parent 2742 | f1192e3474e0 |
| 2746:6aa98a113e6c | 2747:a5da7b6aff8f |
|---|---|
1 (*<*) |
1 (*<*) |
2 theory Paper |
2 theory Paper |
3 imports "../Nominal/Nominal2" "LaTeXsugar" |
3 imports "../Nominal/Nominal2" |
4 "~~/src/HOL/Library/LaTeXsugar" |
|
4 begin |
5 begin |
5 |
6 |
6 consts |
7 consts |
7 fv :: "'a \<Rightarrow> 'b" |
8 fv :: "'a \<Rightarrow> 'b" |
8 abs_set :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" |
9 abs_set :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" |