src/HOL/Sum_Type.ML
changeset 15123 4c49281dc9a8
parent 12921 b7b0daf0d882
equal deleted inserted replaced
15122:4b52eeb62807 15123:4c49281dc9a8