src/HOLCF/Ssum2.thy
changeset 5951 e98c900540f9
parent 2640 ee4dfce170a0
child 12030 46d57d0290a2