src/HOL/Tools/Function/fun_cases.ML
changeset 81527 4f4159c2cad3
parent 70318 9eff9e2dc177
equal deleted inserted replaced
81526:21e042eee085 81527:4f4159c2cad3