src/HOL/Tools/Metis/metis_tactic.ML
changeset 69006 e2d573447efd
parent 67379 c2dfc510a38c
child 69593 3dda49e08b9d