src/HOL/Tools/typedef.ML
changeset 45965 2af982715e5c
parent 45407 a83574606719
child 46947 b8c7eb0c2f89