Nominal/Nominal2.thy
changeset 3227 35bb5b013f0e
parent 3226 780b7a2c50b6
child 3228 040519ec99e9
equal deleted inserted replaced
3226:780b7a2c50b6 3227:35bb5b013f0e
    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