src/HOLCF/explicit_domains/Focus_ex.thy
changeset 2335 e965156e84e3
parent 1479 21eb5e156d91