src/Pure/compress.ML
changeset 25995 21b51f748daf
parent 25697 a4b7eb4e20fd
child 26427 f33d1b522316
equal deleted inserted replaced
25994:d35484265f46 25995:21b51f748daf