src/HOL/Sum.ML
changeset 4200 5a2cd204f8b4
parent 4089 96fba19bcbe2
child 4477 b3e5857d8d99