src/HOL/Tools/function_package/fundef_common.ML
changeset 30076 f3043dafef5f
parent 29922 60a304bc5a07
child 30223 24d975352879