| changeset 66453 | cc19f7ca2ed6 |
| parent 63167 | 0909deb8059b |
| child 80140 | 6d56e85f674e |
| 66452:450cefec7c11 | 66453:cc19f7ca2ed6 |
|---|---|
1 section \<open>Simply-typed lambda-calculus with let and tuple patterns\<close> |
1 section \<open>Simply-typed lambda-calculus with let and tuple patterns\<close> |
2 |
2 |
3 theory Pattern |
3 theory Pattern |
4 imports "../Nominal" |
4 imports "HOL-Nominal.Nominal" |
5 begin |
5 begin |
6 |
6 |
7 no_syntax |
7 no_syntax |
8 "_Map" :: "maplets => 'a \<rightharpoonup> 'b" ("(1[_])") |
8 "_Map" :: "maplets => 'a \<rightharpoonup> 'b" ("(1[_])") |
9 |
9 |