src/HOL/Tools/res_skolem_function.ML
changeset 15872 8336ff711d80
parent 15347 14585bc8fa09
child 16803 014090d1e64b