src/HOL/Tools/metis_tools.ML
changeset 28985 af325cd29b15
parent 28700 fb92b1d1b285
child 29266 4a478f9d2847
equal deleted inserted replaced
28984:060832a1f087 28985:af325cd29b15