src/HOL/Tools/Metis/metis_tactic.ML
changeset 48164 e97369f20c30
parent 47047 10bece4ac87e
child 50694 df8ae0590be2