src/Pure/pure_thy.ML
changeset 74035 ec3249dd63dd
parent 72053 4ed33ea8d957
child 74330 d882abae3379
equal deleted inserted replaced
74034:d6ae3a7d9cb0 74035:ec3249dd63dd