src/Pure/compress.ML
changeset 26436 dfd6947ab5c2
parent 26427 f33d1b522316
child 26463 9283b4185fdf