| changeset 61069 | aefe89038dd2 |
| parent 60580 | 7e741e22d7fc |
| child 61166 | 5976fe402824 |
| 61068:6cb92c2a5ece | 61069:aefe89038dd2 |
|---|---|
3 theory Pattern |
3 theory Pattern |
4 imports "../Nominal" |
4 imports "../Nominal" |
5 begin |
5 begin |
6 |
6 |
7 no_syntax |
7 no_syntax |
8 "_Map" :: "maplets => 'a ~=> 'b" ("(1[_])") |
8 "_Map" :: "maplets => 'a \<rightharpoonup> 'b" ("(1[_])") |
9 |
9 |
10 atom_decl name |
10 atom_decl name |
11 |
11 |
12 nominal_datatype ty = |
12 nominal_datatype ty = |
13 Atom nat |
13 Atom nat |