src/HOL/Algebra/abstract/NatSum.ML
changeset 10168 50be659d4222
parent 8863 77245f4a71ef
child 10962 cda180b1e2e0