src/HOL/Tools/datatype_abs_proofs.ML
changeset 14199 d3b8d972a488
parent 13641 63d1790a43ed
child 14799 a405aadff16c