src/Pure/cterm_items.ML
changeset 78021 ce6e3bc34343
parent 77903 38d0a90e87c1
child 79121 6a84d18fa548