src/HOL/Tools/res_skolem_function.ML
changeset 16240 95cc0e8f8a17
parent 15347 14585bc8fa09
child 16803 014090d1e64b