3 Nominal2_Base Nominal2_Abs Nominal2_FCB |
3 Nominal2_Base Nominal2_Abs Nominal2_FCB |
4 keywords |
4 keywords |
5 "nominal_datatype" :: thy_decl and |
5 "nominal_datatype" :: thy_decl and |
6 "nominal_primrec" "nominal_inductive" :: thy_goal and |
6 "nominal_primrec" "nominal_inductive" :: thy_goal and |
7 "avoids" "binds" |
7 "avoids" "binds" |
8 uses ("nominal_dt_rawfuns.ML") |
|
9 ("nominal_dt_alpha.ML") |
|
10 ("nominal_dt_quot.ML") |
|
11 ("nominal_induct.ML") |
|
12 ("nominal_inductive.ML") |
|
13 ("nominal_function_common.ML") |
|
14 ("nominal_function_core.ML") |
|
15 ("nominal_mutual.ML") |
|
16 ("nominal_function.ML") |
|
17 ("nominal_termination.ML") |
|
18 ("nominal_dt_data.ML") |
|
19 begin |
8 begin |
20 |
9 |
21 use "nominal_dt_data.ML" |
10 ML_file "nominal_dt_data.ML" |
22 ML {* open Nominal_Dt_Data *} |
11 ML {* open Nominal_Dt_Data *} |
23 |
12 |
24 use "nominal_dt_rawfuns.ML" |
13 ML_file "nominal_dt_rawfuns.ML" |
25 ML {* open Nominal_Dt_RawFuns *} |
14 ML {* open Nominal_Dt_RawFuns *} |
26 |
15 |
27 use "nominal_dt_alpha.ML" |
16 ML_file "nominal_dt_alpha.ML" |
28 ML {* open Nominal_Dt_Alpha *} |
17 ML {* open Nominal_Dt_Alpha *} |
29 |
18 |
30 use "nominal_dt_quot.ML" |
19 ML_file "nominal_dt_quot.ML" |
31 ML {* open Nominal_Dt_Quot *} |
20 ML {* open Nominal_Dt_Quot *} |
32 |
21 |
33 (*****************************************) |
22 (*****************************************) |
34 (* setup for induction principles method *) |
23 (* setup for induction principles method *) |
35 use "nominal_induct.ML" |
24 ML_file "nominal_induct.ML" |
36 method_setup nominal_induct = |
25 method_setup nominal_induct = |
37 {* NominalInduct.nominal_induct_method *} |
26 {* NominalInduct.nominal_induct_method *} |
38 {* nominal induction *} |
27 {* nominal induction *} |
39 |
28 |
40 (****************************************************) |
29 (****************************************************) |
41 (* inductive definition involving nominal datatypes *) |
30 (* inductive definition involving nominal datatypes *) |
42 use "nominal_inductive.ML" |
31 ML_file "nominal_inductive.ML" |
43 |
32 |
44 |
33 |
45 (***************************************) |
34 (***************************************) |
46 (* forked code of the function package *) |
35 (* forked code of the function package *) |
47 (* for defining nominal functions *) |
36 (* for defining nominal functions *) |
48 use "nominal_function_common.ML" |
37 ML_file "nominal_function_common.ML" |
49 use "nominal_function_core.ML" |
38 ML_file "nominal_function_core.ML" |
50 use "nominal_mutual.ML" |
39 ML_file "nominal_mutual.ML" |
51 use "nominal_function.ML" |
40 ML_file "nominal_function.ML" |
52 use "nominal_termination.ML" |
41 ML_file "nominal_termination.ML" |
53 |
42 |
54 ML {* |
43 ML {* |
55 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
44 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
56 val simp_attr = Attrib.internal (K Simplifier.simp_add) |
45 val simp_attr = Attrib.internal (K Simplifier.simp_add) |
57 val induct_attr = Attrib.internal (K Induct.induct_simp_add) |
46 val induct_attr = Attrib.internal (K Induct.induct_simp_add) |