src/Pure/compress.ML
changeset 25898 d8f17d8cf9d4
parent 25697 a4b7eb4e20fd
child 26427 f33d1b522316
equal deleted inserted replaced
25897:e9d45709bece 25898:d8f17d8cf9d4