2 imports |
2 imports |
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 ("induction_schema.ML") |
7 ("nominal_induct.ML") |
8 begin |
8 begin |
9 |
9 |
10 use "induction_schema.ML" |
|
11 |
10 |
12 use "nominal_dt_rawfuns.ML" |
11 use "nominal_dt_rawfuns.ML" |
13 ML {* open Nominal_Dt_RawFuns *} |
12 ML {* open Nominal_Dt_RawFuns *} |
14 |
13 |
15 use "nominal_dt_alpha.ML" |
14 use "nominal_dt_alpha.ML" |
16 ML {* open Nominal_Dt_Alpha *} |
15 ML {* open Nominal_Dt_Alpha *} |
17 |
16 |
18 use "nominal_dt_quot.ML" |
17 use "nominal_dt_quot.ML" |
19 ML {* open Nominal_Dt_Quot *} |
18 ML {* open Nominal_Dt_Quot *} |
20 |
19 |
|
20 (*****************************************) |
|
21 (* setup for induction principles method *) |
|
22 use "nominal_induct.ML" |
|
23 method_setup nominal_induct = |
|
24 {* NominalInduct.nominal_induct_method *} |
|
25 {* nominal induction *} |
21 |
26 |
22 ML {* |
27 ML {* |
23 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
28 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
24 val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add) |
29 val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add) |
25 val simp_attr = Attrib.internal (K Simplifier.simp_add) |
30 val simp_attr = Attrib.internal (K Simplifier.simp_add) |