equal
deleted
inserted
replaced
1 theory Perm |
1 theory Perm |
2 imports |
2 imports |
3 "../Nominal-General/Nominal2_Base" |
3 "../Nominal-General/Nominal2_Base" |
4 "../Nominal-General/Nominal2_Atoms" |
4 "../Nominal-General/Nominal2_Atoms" |
5 "Nominal2_FSet" "Abs" |
5 "../Nominal-General/Nominal2_Eqvt" |
6 uses ("nominal_dt_rawperm.ML") |
6 "Nominal2_FSet" |
|
7 "Abs" |
|
8 (*uses ("nominal_dt_rawperm.ML") |
7 ("nominal_dt_rawfuns.ML") |
9 ("nominal_dt_rawfuns.ML") |
8 ("nominal_dt_alpha.ML") |
10 ("nominal_dt_alpha.ML")*) |
9 begin |
11 begin |
10 |
12 |
11 use "nominal_dt_rawperm.ML" |
13 use "nominal_dt_rawperm.ML" |
12 ML {* open Nominal_Dt_RawPerm *} |
14 ML {* open Nominal_Dt_RawPerm *} |
13 |
15 |