src/HOL/Sum.thy
changeset 2183 8d42a7bccf0b
parent 1558 9c6ebfab4e05
child 2212 bd705e9de196