src/Pure/compress.ML
changeset 17003 b902e11b3df1
parent 16981 2ae3f621d076
child 17221 6cd180204582
equal deleted inserted replaced
17002:fb9261990ffe 17003:b902e11b3df1