src/HOL/Sum.thy
changeset 2159 e650a3f6f600
parent 1558 9c6ebfab4e05
child 2212 bd705e9de196