src/HOL/typedef.ML
changeset 2754 59bd96046ad6
parent 2238 c72a23bbe762
child 2851 b6a5780e36b9