src/HOL/Tools/Metis/metis_tactics.ML
changeset 42174 d0be2722ce9f
parent 40665 1a65f0c74827
child 42336 d63d43e85879