src/HOL/Tools/function_package/fundef_proof.ML
changeset 19759 2d0896653e7a
parent 19583 c5fa77b03442
child 19770 be5c23ebe1eb