src/HOL/Sum_Type.ML
changeset 15220 cc88c8ee4d2f
parent 12921 b7b0daf0d882
equal deleted inserted replaced
15219:fb4b5c2cca8b 15220:cc88c8ee4d2f