src/Pure/cterm_items.ML
changeset 80949 97924a26a5c3
parent 79162 c1bbaa0d89b4
child 81959 fae61f1c8113
equal deleted inserted replaced
80948:572970d15ab0 80949:97924a26a5c3