src/HOL/Tools/Metis/metis_tactic.ML
changeset 57978 8f4a332500e4
parent 57408 39b3562e9edc
child 58818 ee85e7b82d00