src/HOL/Tools/Metis/metis_translate.ML
changeset 42685 7a5116bd63b7
parent 42650 552eae49f97d
child 42727 f365f5138771
equal deleted inserted replaced
42684:2123b2608b14 42685:7a5116bd63b7