src/HOL/Tools/Metis/metis_translate.ML
changeset 45570 6d95a66cce00
parent 45569 eb30a5490543