src/HOL/Sum.thy
changeset 1444 23ceb1dc9755
parent 1423 5726a8243d3f
child 1475 7f5a4cd08209