src/HOL/Sum.ML
changeset 4732 10af4886b33f
parent 4535 f24cebc299e4
child 4830 bd73675adbed
equal deleted inserted replaced
4731:0196377b5703 4732:10af4886b33f