equal
deleted
inserted
replaced
45 val simp_attr = Attrib.internal (K Simplifier.simp_add) |
45 val simp_attr = Attrib.internal (K Simplifier.simp_add) |
46 val induct_attr = Attrib.internal (K Induct.induct_simp_add) |
46 val induct_attr = Attrib.internal (K Induct.induct_simp_add) |
47 *} |
47 *} |
48 |
48 |
49 section{* Interface for nominal_datatype *} |
49 section{* Interface for nominal_datatype *} |
50 |
|
51 ML {* print_depth 50 *} |
|
52 |
50 |
53 ML {* |
51 ML {* |
54 fun get_cnstrs dts = |
52 fun get_cnstrs dts = |
55 map snd dts |
53 map snd dts |
56 |
54 |