src/HOL/Tools/typedef.ML
changeset 67906 9cc32b18c785
parent 67664 ad2b3e330c27
child 68264 bb9a3be6952a