src/HOL/Tools/function_package/fundef_common.ML
changeset 30629 5cd9b19edef3
parent 30560 0cc3b7f03ade
child 30787 5b7a5a05c7aa