src/HOL/Tools/datatype_abs_proofs.ML
changeset 15131 c69542757a4d
parent 14981 e73f8140af78
child 15459 16dd63c78049