src/HOL/Tools/function_package/auto_term.ML
changeset 21258 62f25a96f0c1
parent 21104 b6ab939147eb
child 21319 cf814e36f788