src/HOL/typedef.ML
changeset 1444 23ceb1dc9755
parent 1264 3eb91524b938
child 1475 7f5a4cd08209