src/HOL/Tools/metis_tools.ML
changeset 24819 7d8e0a47392e
parent 24500 5e135602f660
child 24827 646bdc51eb7d
equal deleted inserted replaced
24818:d07e56a9a0c2 24819:7d8e0a47392e