src/HOL/HOLCF/FOCUS/Buffer.thy
changeset 57978 8f4a332500e4
parent 42151 4da4fc77664b
child 58305 57752a91eec4