equal
deleted
inserted
replaced
6 "Nominal2_FSet" |
6 "Nominal2_FSet" |
7 "Abs" |
7 "Abs" |
8 uses ("nominal_dt_rawperm.ML") |
8 uses ("nominal_dt_rawperm.ML") |
9 ("nominal_dt_rawfuns.ML") |
9 ("nominal_dt_rawfuns.ML") |
10 ("nominal_dt_alpha.ML") |
10 ("nominal_dt_alpha.ML") |
|
11 ("nominal_dt_quot.ML") |
11 begin |
12 begin |
12 |
13 |
13 use "nominal_dt_rawperm.ML" |
14 use "nominal_dt_rawperm.ML" |
14 ML {* open Nominal_Dt_RawPerm *} |
15 ML {* open Nominal_Dt_RawPerm *} |
15 |
16 |
16 use "nominal_dt_rawfuns.ML" |
17 use "nominal_dt_rawfuns.ML" |
17 ML {* open Nominal_Dt_RawFuns *} |
18 ML {* open Nominal_Dt_RawFuns *} |
18 |
19 |
19 use "nominal_dt_alpha.ML" |
20 use "nominal_dt_alpha.ML" |
20 ML {* open Nominal_Dt_Alpha *} |
21 ML {* open Nominal_Dt_Alpha *} |
|
22 |
|
23 use "nominal_dt_quot.ML" |
|
24 ML {* open Nominal_Dt_Quot *} |
|
25 |
21 |
26 |
22 (* permutations for quotient types *) |
27 (* permutations for quotient types *) |
23 |
28 |
24 ML {* |
29 ML {* |
25 fun quotient_lift_consts_export qtys spec ctxt = |
30 fun quotient_lift_consts_export qtys spec ctxt = |
31 val defs = Morphism.fact morphism defs_loc |
36 val defs = Morphism.fact morphism defs_loc |
32 in |
37 in |
33 (ts, defs, ctxt') |
38 (ts, defs, ctxt') |
34 end |
39 end |
35 *} |
40 *} |
|
41 |
|
42 |
36 |
43 |
37 ML {* |
44 ML {* |
38 fun define_lifted_perms qtys full_tnames name_term_pairs thms thy = |
45 fun define_lifted_perms qtys full_tnames name_term_pairs thms thy = |
39 let |
46 let |
40 val lthy = |
47 val lthy = |