src/HOL/Tools/datatype_abs_proofs.ML
changeset 13076 70704dd48bd5
parent 12910 f5bceeec9d91
child 13641 63d1790a43ed