src/HOL/Tools/typedef_package.ML
changeset 24841 df8448bc7a8b
parent 24830 a7b3ab44d993
child 24861 cc669ca5f382