src/HOL/Sum_Type.ML
changeset 15096 be1d3b8cfbd5
parent 12921 b7b0daf0d882