src/HOLCF/Sprod2.thy
changeset 9927 7a9652294fe0
parent 2640 ee4dfce170a0
child 12030 46d57d0290a2