equal
deleted
inserted
replaced
4 uses ("nominal_dt_rawfuns.ML") |
4 uses ("nominal_dt_rawfuns.ML") |
5 ("nominal_dt_alpha.ML") |
5 ("nominal_dt_alpha.ML") |
6 ("nominal_dt_quot.ML") |
6 ("nominal_dt_quot.ML") |
7 ("nominal_induct.ML") |
7 ("nominal_induct.ML") |
8 ("nominal_inductive.ML") |
8 ("nominal_inductive.ML") |
|
9 ("nominal_function_core.ML") |
|
10 ("nominal_mutual.ML") |
|
11 ("nominal_function.ML") |
9 begin |
12 begin |
10 |
|
11 |
13 |
12 use "nominal_dt_rawfuns.ML" |
14 use "nominal_dt_rawfuns.ML" |
13 ML {* open Nominal_Dt_RawFuns *} |
15 ML {* open Nominal_Dt_RawFuns *} |
14 |
16 |
15 use "nominal_dt_alpha.ML" |
17 use "nominal_dt_alpha.ML" |
27 |
29 |
28 (****************************************************) |
30 (****************************************************) |
29 (* inductive definition involving nominal datatypes *) |
31 (* inductive definition involving nominal datatypes *) |
30 use "nominal_inductive.ML" |
32 use "nominal_inductive.ML" |
31 |
33 |
|
34 |
|
35 (***************************************) |
|
36 (* forked code of the function package *) |
|
37 (* for defining nominal functions *) |
|
38 use "nominal_function_core.ML" |
|
39 use "nominal_mutual.ML" |
|
40 use "nominal_function.ML" |
32 |
41 |
33 ML {* |
42 ML {* |
34 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
43 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
35 val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add) |
44 val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add) |
36 val simp_attr = Attrib.internal (K Simplifier.simp_add) |
45 val simp_attr = Attrib.internal (K Simplifier.simp_add) |