src/Pure/term_items.ML
changeset 80949 97924a26a5c3
parent 80583 9a40ec7a2027
child 81259 1c2be1fca2bd