src/Pure/cterm_items.ML
changeset 74913 c2a2be496f35
parent 74272 0f3ca0cd8071
child 77903 38d0a90e87c1