src/Pure/compress.ML
changeset 17115 127aa3d49129
parent 16981 2ae3f621d076
child 17221 6cd180204582