src/HOL/Tools/typedef.ML
changeset 40534 9e196062bf88
parent 38757 2b3e054ae6fc
child 42290 b1f544c84040