src/HOL/Tools/typedef.ML
changeset 68475 b6e48841d0a5
parent 68264 bb9a3be6952a
child 69829 3bfa28b3a5b2