| changeset 1774 | c34347ec7ab3 |
| parent 1683 | f78c820f67c3 |
| child 1871 | c704d129862b |
| 1773:c0eac04ae3b4 | 1774:c34347ec7ab3 |
|---|---|
1 theory Perm |
1 theory Perm |
2 imports "Nominal2_Atoms" |
2 imports "../Nominal-General/Nominal2_Atoms" |
3 begin |
3 begin |
4 |
4 |
5 ML {* |
5 ML {* |
6 open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *) |
6 open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *) |
7 fun permute ty = Const (@{const_name permute}, @{typ perm} --> ty --> ty); |
7 fun permute ty = Const (@{const_name permute}, @{typ perm} --> ty --> ty); |