src/Pure/compress.ML
changeset 26179 bc5d582d6cfe
parent 25697 a4b7eb4e20fd
child 26427 f33d1b522316