src/Pure/cterm_items.ML
changeset 74561 8e6c973003c8
parent 74272 0f3ca0cd8071
child 77903 38d0a90e87c1