src/HOL/Tools/typedef.ML
changeset 46746 a10dcc985e8d
parent 45407 a83574606719
child 46947 b8c7eb0c2f89