src/Pure/cterm_items.ML
changeset 75886 ccdca89e19d6
parent 74272 0f3ca0cd8071
child 77903 38d0a90e87c1
equal deleted inserted replaced
75885:8342cba8eae8 75886:ccdca89e19d6