src/HOL/Tools/Metis/metis_translate.ML
changeset 42557 ae0deb39a254
parent 42544 75cb06eee990
child 42561 23ddc4e3d19c