3 Nominal2_Base Nominal2_Eqvt Nominal2_Abs |
3 Nominal2_Base Nominal2_Eqvt Nominal2_Abs |
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 begin |
9 begin |
9 |
10 |
10 |
11 |
11 use "nominal_dt_rawfuns.ML" |
12 use "nominal_dt_rawfuns.ML" |
12 ML {* open Nominal_Dt_RawFuns *} |
13 ML {* open Nominal_Dt_RawFuns *} |
14 use "nominal_dt_alpha.ML" |
15 use "nominal_dt_alpha.ML" |
15 ML {* open Nominal_Dt_Alpha *} |
16 ML {* open Nominal_Dt_Alpha *} |
16 |
17 |
17 use "nominal_dt_quot.ML" |
18 use "nominal_dt_quot.ML" |
18 ML {* open Nominal_Dt_Quot *} |
19 ML {* open Nominal_Dt_Quot *} |
|
20 |
|
21 |
19 |
22 |
20 (*****************************************) |
23 (*****************************************) |
21 (* setup for induction principles method *) |
24 (* setup for induction principles method *) |
22 use "nominal_induct.ML" |
25 use "nominal_induct.ML" |
23 method_setup nominal_induct = |
26 method_setup nominal_induct = |
24 {* NominalInduct.nominal_induct_method *} |
27 {* NominalInduct.nominal_induct_method *} |
25 {* nominal induction *} |
28 {* nominal induction *} |
|
29 |
|
30 (****************************************************) |
|
31 (* inductive definition involving nominal datatypes *) |
|
32 use "nominal_inductive.ML" |
|
33 |
26 |
34 |
27 ML {* |
35 ML {* |
28 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
36 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
29 val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add) |
37 val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add) |
30 val simp_attr = Attrib.internal (K Simplifier.simp_add) |
38 val simp_attr = Attrib.internal (K Simplifier.simp_add) |