changeset 66453 | cc19f7ca2ed6 |
parent 63167 | 0909deb8059b |
66452:450cefec7c11 | 66453:cc19f7ca2ed6 |
---|---|
1 theory Lam_Funs |
1 theory Lam_Funs |
2 imports "../Nominal" |
2 imports "HOL-Nominal.Nominal" |
3 begin |
3 begin |
4 |
4 |
5 text \<open> |
5 text \<open> |
6 Provides useful definitions for reasoning |
6 Provides useful definitions for reasoning |
7 with lambda-terms. |
7 with lambda-terms. |