src/HOL/Tools/datatype_abs_proofs.ML
changeset 19818 5c5c1208a3fa
parent 19233 77ca20b0ed77
child 20046 9c8909fc5865