src/HOL/typedef.ML
changeset 2250 891eb76b8045
parent 2238 c72a23bbe762
child 2851 b6a5780e36b9