src/HOL/Tools/datatype_case.ML
changeset 31136 85d04515abb3
parent 29623 1219985d24b5
equal deleted inserted replaced
31135:e2d777dcf161 31136:85d04515abb3