src/HOL/mono.ML
changeset 9993 c0f7fb6e538e
parent 9969 4753185f1dd2
child 10832 e33b47e4246d