src/HOL/Sum.thy
changeset 10168 50be659d4222
parent 9311 ab5b24cbaa16