src/HOL/HOLCF/FOCUS/Buffer.thy
changeset 45463 9a588a835c1e
parent 42151 4da4fc77664b
child 58305 57752a91eec4