src/HOL/Tools/Function/fun_cases.ML
changeset 53810 69e8ba502eda
parent 53670 5ccee1cb245a
child 53991 d8f7f3d998de