src/HOL/Algebra/abstract/NatSum.ML
changeset 10146 e89309dde9d3
parent 8863 77245f4a71ef
child 10962 cda180b1e2e0