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