src/HOL/Sum_Type.ML
changeset 14151 b8bb6a6a2c46
parent 12921 b7b0daf0d882
equal deleted inserted replaced
14150:9a23e4eb5eb3 14151:b8bb6a6a2c46