src/Pure/pure_syn.ML
changeset 80972 7c1e73540990
parent 74881 1e84ae3e886e
equal deleted inserted replaced
80971:2c57002d98e4 80972:7c1e73540990