src/HOL/Sum.ML
changeset 9950 879e88b1e552
parent 9311 ab5b24cbaa16
equal deleted inserted replaced
9949:1741a61d4b33 9950:879e88b1e552