equal
deleted
inserted
replaced
15 use "nominal_dt_quot.ML" |
15 use "nominal_dt_quot.ML" |
16 ML {* open Nominal_Dt_Quot *} |
16 ML {* open Nominal_Dt_Quot *} |
17 |
17 |
18 |
18 |
19 section{* Interface for nominal_datatype *} |
19 section{* Interface for nominal_datatype *} |
20 |
|
21 ML {* |
|
22 (* attributes *) |
|
23 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
|
24 val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add) |
|
25 val simp_attr = Attrib.internal (K Simplifier.simp_add) |
|
26 |
|
27 *} |
|
28 |
20 |
29 ML {* print_depth 50 *} |
21 ML {* print_depth 50 *} |
30 |
22 |
31 ML {* |
23 ML {* |
32 fun get_cnstrs dts = |
24 fun get_cnstrs dts = |