src/Pure/compress.ML
changeset 26629 6e93fbd4c96a
parent 26463 9283b4185fdf