src/HOL/mono.ML
changeset 1251 81fc4d8e3eda
parent 923 ff1574a81019
child 1264 3eb91524b938