src/Pure/compress.ML
changeset 23730 8866c87d1a16
parent 22846 fb79144af9a3
child 23922 707639e9497d
equal deleted inserted replaced
23729:d1ba656978c5 23730:8866c87d1a16