src/HOL/Tools/res_skolem_function.ML
changeset 16123 1381e90c2694
parent 15347 14585bc8fa09
child 16803 014090d1e64b